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 :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.