### 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.