Major Section: MISCELLANEOUS
Example and General Form: ACL2 !>:redef- ACL2 p!>
This macro, for system hackers only, is a convenient way to reverse the
:redef+. See redef+.
Note that this macro starts by executing
:redef+, in case some effects of
:redef+ have already been removed or perhaps
not been done at all.