Set-raw-proof-format
Print runes as lists in proof output from simplification
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.
To obtain the current raw-proof-format (t if that format is active,
nil if not), evaluate (@ raw-proof-format).
