Major Section: SWITCHES-PARAMETERS-AND-MODES
General Forms: (set-raw-proof-format t) :set-raw-proof-format t (set-raw-proof-format nil) :set-raw-proof-format nilThis command affects output from the theorem prover only when
'proveoutput is not inhibited (see set-inhibit-output-lst) and gag-mode is off (see set-gag-mode). Calling this macro with value
tas shown above will cause simplification steps from proof output, including steps from preprocess (see simple), to print the list of runes used in a list format, rather than in the English proof commentary. This ``raw'' format can be handy when you want to use that list as a basis for
hintsthat you construct for a subsequent proof attempt.