text: 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.