SET-RAW-PROOF-FORMAT
print runes as lists in proof output from simplification
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 nil
This command affects output from the theorem prover only when 'prove
output is not inhibited (see set-inhibit-output-lst) and gag-mode is off
(see set-gag-mode). Calling this macro with value t as 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 hints that you construct for a
subsequent proof attempt.
