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
improved.
A slight change has been made to the proof-checker for commands
promote, casesplit, equiv, and =, 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.
A new proof-checker command, runes, has been added. It reports
the runes that have participated in the interactive proof up to the
current point.