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.