Major Section: MISCELLANEOUS
Example and General Form: ACL2 !>:redef- ACL2 p!>
This macro, for system hackers only, is a convenient way to reverse the
effects of :redef+. See redef+. We do not guarantee that :redef-
will restore everything one might expect to its state before the earlier
:redef+. To see exactly what :redef- does, look at its code, for
example by evaluating :trans1 (redef-)
