REDEF-

turn off system hacker's redefinition command
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-)