Set-inhibited-summary-types
Control which parts of the summary are printed
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*, which is (errors form header hint-events
redundant rules splitter-rules steps
system-attachments time value warnings).
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.
