'proveoutput is inhibited
Major Section: SWITCHES-PARAMETERS-AND-MODES
General Forms: (set-print-clause-ids t) :set-print-clause-ids t (set-print-clause-ids nil) :set-print-clause-ids nilThis command affects output from the theorem prover only when
'proveoutput is inhibited; see set-inhibit-output-lst. Calling this macro with value
tas shown above will cause subsequent proof attempts with
'proveoutput inhibited to print the subgoal number, so that you can see the progress of the proof; value
nilreverts to the default behavior, where this is not the case. On a related note, we point out that you can cause output to be saved for later display; see pso and see pso!.