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.