REMOVE-OVERRIDE-HINTS_bang_.html -- ACL2 Version 6.2

REMOVE-OVERRIDE-HINTS!

delete non-locally from the list of override-hints

Major Section:  SWITCHES-PARAMETERS-AND-MODES

Remove-override-hints! is the same as remove-override-hints, except that the former is not local to books or encapsulate events in which it occurs. See remove-override-hints; also see add-override-hints and see set-override-hints.