Note-2-8-proof-builder
ACL2 Version 2.8 Notes on proof-builder Changes
Added new proof-builder 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-builder-commands.
The proof-builder 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-builder-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.
