ACL2 Version 2.6 Notes on proof-builder Changes
The proof-builder command =, when used with no arguments, now
reports which hypothesis is being used.
The output from proof-builder command type-alist has been
A slight change has been made to the proof-builder 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-builder command print-all-concs that
prints all the conclusions of the unproved goals.
A new proof-builder command, runes, has been added. It
reports the runes that have participated in the interactive proof up to
the current point.