Major Section: MISCELLANEOUS
Example and General Form: ACL2 !>:redef! ACL2 p!>This command sets
'(:warn! . :overwrite)sets the default defun-mode to
program, and invokes
(set-state-ok t). It also introduces
(defttag :redef!), so that redefinition of system functions will be permitted; see defttag.
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!