Major Section: EVENTS
Examples: (add-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 add-default-hints! for a corresponding non-local event).
General Form: (add-default-hints lst)where
lst is a list. Generally speaking, the element of
lst should be suitable for use as computed-hints.
This event is completely analogous to set-default-hints, the difference
being that add-default-hints appends the indicated hints to the list of
default hints, rather than replacing the default hints with the
indicated hints.
Finally, note that the effects of set-default-hints,
add-default-hints, and 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 set-default-hints!,
add-default-hints!, or remove-default-hints!.
