Major Section: MISCELLANEOUS
Examples: ACL2 !>(default-hints (w state)) ((computed-hint-1 clause) (computed-hint-2 clause stable-under-simplificationp))The value returned by this function is added to the right of the
:hints argument of every defthm and thm command, and to
hints provided to defuns as well (:hints, :guard-hints, and
(for ACL2(r)) :std-hints).
See set-default-hints for a more general discussion. Advanced users only:
see override-hints for an advanced variant of default hints that are not
superseded by :hints arguments.
