NOTE-2-8-PROOF-CHECKER

ACL2 Version 2.8 Notes on Proof-checker Changes
Major Section:  NOTE-2-8

Added new proof-checker commands wrap1, wrap, and wrap-induct. Wrap replaces multiple goals by their conjunction: (wrap instr1 instr2 ...) employs wrap1 so that the indicated instructions create only at most one new goal. Wrap-induct is a simple example of the use of wrap, so that induction creates only one goal (the conjunction of the base and induction steps). Wrap1 can be used immediately after a prover call (bash, prove, reduce, bdd, or induct) to collapse the new goals into one. See proof-checker-commands.

The proof-checker command = failed to work as expected when a governing IF-test of the current term is T. This has been fixed (by fixing source function conjuncts-of). Thanks to Yoann Padioleau for bringing this problem to our attention.

The type-alist command now takes optional arguments that control whether or not the governors and/or conclusion are used in computing the context that is printed (see proof-checker-commands, specifically subtopic type-alist). Thanks to Rob Sumners for suggesting this improvement.

The macro toggle-pc-macro has always taken an optional second argument of atomic-macro or macro. However, this was not clearly documented, and those two symbols had to be in the ACL2 package. Both of these problems have been remedied. Thanks to John Erickson for bringing the lack of documentation of the second argument to our attention.