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.

See set-default-hints for a more general discussion.