Major Section: MISCELLANEOUS
Example and General Form: ACL2 !>:redef! ACL2 p!>This command sets
ld-redefinition-action to '(: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!