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
hintsargument of every
thmcommand, and to hints provided to
defuns as well (
:guard-hints, and (for ACL2(r))
See set-default-hints for a more general discussion.