DEFAULT-HINTS

a list of hints added to every proof attempt
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.