Major Section: EVENTS
Examples: (remove-default-hints '((computed-hint-1 clause) (computed-hint-2 clause stable-under-simplificationp)))
Note: This is an event! It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded. It is
local to the book or
encapsulate form in which it occurs
(see remove-default-hints! for a corresponding non-local event).
General Form: (remove-default-hints lst)where
lstis a list. Generally speaking, the element of
lstshould be suitable for use as
computed-hints. Also see add-default-hints.
If some elements of the given list do not belong to the existing default hints, they will simply be ignored by this event.
Finally, note that the effects of
remove-default-hints are local to the
book in which they appear. Thus, users who include a book with such forms
will not have their default hints affected by such forms. In order to export
the effect of setting the default hints, use