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+.

Note that this macro starts by executing :redef+, in case some effects of a previous :redef+ have already been removed or perhaps :redef+ had not been done at all.