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)
.
This is the ACL2 system hacker's redefinition command. Note that
even system functions can be redefined with a mere warning. Be
careful!