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.