A common way to set ld-redefinition-action
Example and General Form: ACL2 !>:redef
This command sets ld-redefinition-action to
This command allows redefinition of functions and other events without undoing, but with a query that requires the user to acknowledge that the redefinition is intentional. To avoid that query, see redef!. For more options and an important warning about the danger of using redefinition, including possible unsoundness, see ld-redefinition-action.