Major Section: SWITCHES-PARAMETERS-AND-MODES
Example: (set-inhibited-summary-types '(rules time))Note: This is not an event. Rather, it changes the state, in analogy to
set-inhibit-output-lst
.
General Form: (set-inhibited-summary-types form)where form evaluates to a true-list of symbols, each of which is among the values of the constant
*summary-types*
, i.e.: header
, form
,
rules
, hint-events
warnings
, time
, steps
, and value
.
Each specified type inhibits printing of the corresponding portion of the
summaries printed at the conclusions of events, where header
refers
to an initial newline followed by the line containing just the word
Summary
.Note the distinction between rules
and hint-events
. Rules
provides a record of automatic rule usage by the prover, while
hint-events
shows the names of events given to :USE
or :BY
hints, as well as clause-processor functions given to
:CLAUSE-PROCESSOR
hints that have an effect on the proof.
Also see set-inhibit-output-lst. Note that set-inhibited-summary-types
has no effect when summary
is one of the types inhibited by
set-inhibit-output-lst, because in that case none of the summary will be
printed.
To control summary types for a single event, see with-output.