		Search-engine friendly clone of the ACL2 documentation.

Defttag

Set-deferred-ttag-notes

Modify the verbosity of TTAG NOTE printing

General Form:
(set-deferred-ttag-notes val state)

where val is t or nil.

See defttag for a discussion of trust tags (ttags). By default, a ``TTAG NOTE'' is printed in order to indicate reliance on a ttag. When many such notes are printed, it may be desirable to avoid seeing them all. Upon evaluation of the form

(set-deferred-ttag-notes t state)

ACL2 will enter a deferred mode for the printing of ttag notes. In this mode, only the first ttag note is printed for each top-level command, and the remainder are summarized before the next top-level prompt (if any) is printed, hence before the next command is evaluated. That summary is merely a list of ttags, but the summary explains that the full ttag notes may be printed with the command (show-ttag-notes).

Note that (show-ttag-notes) spares you duplicate ttag notes. If you want to see every ttag note as it would normally appear, for maximum security, do not evaluate the command (set-deferred-ttag-notes t state). You can undo the effect of this command, returning to an immediate mode for printing ttag notes, by evaluating:

(set-deferred-ttag-notes nil state)