Major Section: NOTE-2-6
The proof-checker command
=, when used with no arguments, now
reports which hypothesis is being used.
The output from proof-checker command
type-alist has been
A slight change has been made to the proof-checker for commands
=, so that terms of the form
(if x nil y) are recognized as conjunctions,
(and (not x) y).
Thanks to Pete Manolios for suggesting that we consider such a change.
There is a new proof-checker command
print-all-concs that prints
all the conclusions of the unproved goals.
runes, has been added. It reports
the runes that have participated in the interactive proof up to the