Major Section: MISCELLANEOUS
Example and General Form: ACL2 !>:redef+ ACL2 p!>
This command is intended only for system hackers, not typical users. It
'(:warn! . :overwrite), sets the
default defun-mode to
program, and invokes
t. It also introduces
(defttag :redef+), so that
redefinition of system functions will be permitted; see defttag. Finally,
it removes as untouchable all variables and functions.
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!