Major Section: MISCELLANEOUS
Example and General Form: ACL2 !>:redef+ ACL2 p!>
This command is intended only for system hackers, not typical users. It
sets ld-redefinition-action to '(:warn! . :overwrite), sets the
default defun-mode to :program, and invokes set-state-ok
with value t. It also introduces (defttag :redef+), so that
redefinition of system functions will be permitted; see defttag. Finally,
it removes as untouchable (see push-untouchable) all variables and
functions.
WARNING: If the form (redef+) is used in a book, then including the book
can leave you in a state in which dangerous actions are allowed,
specifically: redefinition, and access to functions and variables normally
prohibited because they are untouchable. To avoid this problem, insert the
form (redef-) into your book after (redef+).
To see the code for redef+, evaluate :trans1 (redef+). This
command is intended for those who are modifying ACL2 source code
definitions. Thus, note that even system functions can be redefined with a
mere warning. Be careful!
