NOTE-2-6-PROOF-CHECKER

ACL2 Version 2.6 Notes on Proof-checker Changes
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.