Major Section: MISCELLANEOUS
Example and General Form: ACL2 !>:redef!This command sets
'(:warn! . :overwrite).
This command allows redefinition of functions and other events without
undoing, but with a warning. The command
redef is similar, but
queries the user first before doing the redefinition. For more related
options, see ld-redefinition-action.