SET-PRINT-CLAUSE-IDS

cause subgoal numbers to be printed when 'prove output is inhibited 
Major Section:  OTHER


General Forms:
(set-print-clause-ids t)
:set-print-clause-ids t
(set-print-clause-ids nil)
:set-print-clause-ids nil
This command affects output from the theorem prover only when 'prove output is inhibited; see set-inhibit-output-lst. Calling this macro with value t as shown above will cause subsequent proof attempts with 'prove output inhibited to print the subgoal number, so that you can see the progress of the proof; value nil reverts 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!.