Major Section: NOTE-2-8
Added new proof-checker commands
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 (
induct) to collapse the new goals into one. See proof-checker-commands.
The proof-checker command
= failed to work as expected when a
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.
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.
toggle-pc-macro has always taken an optional second argument
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.