DEFAULT-HINTS-TABLE

a table used to provide hints for proofs
Major Section:  EVENTS

Please see set-default-hints, see add-default-hints, and see remove-default-hints for how to use this table. For completeness, we mention here that under the hood, these events all update the default-hints-table by updating its unique key, t, for example as follows.

(table default-hints-table t
       '((computed-hint-1 clause)
         (computed-hint-2 clause
                          stable-under-simplificationp)))

The use of default hints is explained elsewhere; see set-default-hints.