suppressing or turning on specified output for an event
Major Section:  EVENTS

   :off summary ; turn off the event summary when evaluating the following:
   (in-theory (disable name)))

General Form: (with-output :key1 val1 ... :keyk valk form)

where each :keyi is either :off or :on and either vali is either :all or else a symbol or non-empty list of symbols representing output types that can be inhibited (see set-inhibit-output-lst). The result of evaluating the General Form above is to evaluate form, but in an environment where the current set of inhibited output types is modified: if :on :all is specified, then all output is turned on except as specified by :off; else if :off :all is specified, then all output is inhibited except as specified by :on; and otherwise, the currently-inhibited output types are reduced as specified by :on and then extended as specified by :off.