Major Section: RELEASE-NOTES
The Version 2.7 notes are divided into the subtopics below. Here we give only a brief summary of a few of the changes that seem most likely to impact existing proofs. Not included in this brief summary, but included in the subtopics, are descriptions of improvements (including bug fixes and new functionality) that should not get in the way of existing proof efforts.
In particular, please see note-2-7-new-functionality for discussion of a number of new features that you may find useful.
Acknowledgements and elaboration, as well as other changes, can be found in the subtopics listed below.
o Bug fixes (see note-2-7-bug-fixes):
+ Three soundness bugs were fixed. These bugs were probably rarely hit, so users may well not notice these changes.
:defaxioms-okp t) if there are
defaxiom) events in the book or any included sub-books.
:byhints refer to a definition, they now use the original body of that definition rather than the simplfied (``normalized'') body.
ldis applied to a stringp file name, it now temporarily sets the connected book directory (see cbd) to the directory of that file while evaluating forms in that file.
o New functionality (see note-2-7-new-functionality):
+ ACL2 now works harder to apply
linearrules with free variables in the hypotheses. See note-2-7-new-functionality, in particular its first two paragraphs, for details. Forward-chaining also does more with free variables.
o Changes in proof engine (see note-2-7-proofs):
+ Some prover heuristics have changed slightly. Among other consequences, this can cause subgoal hints to change. For example, suppose that the Version_2.6 proof of a particular theorem generated "Subgoal 2" and "Subgoal 1" while Version_2.7 only generates the second of these. Then a subgoal hint attached to "Subgoal 1" in Version_2.6 would have to be attached to "Goal'" in Version_2.7. (See goal-spec.) The full topic has details (see note-2-7-proofs).
o Changes in rules and definitions (see note-2-7-rules):
+ The package name of a generated variable has changed for
o Guard-related changes (see note-2-7-guards):
Guardverification formerly succeeded in a few cases where it should have failed.
+ Guards generated from type declarations now use functions
unsigned-byte-p, now defined in source file
axioms.lispand formerly defined rather similarly under
o Proof-checker changes (see note-2-7-proof-checker):
+ See the above doc topic.
o System-level changes (see note-2-7-system):
+ See the above doc topic.
o Other changes (see note-2-7-other):
+ A new
invisible-fns-table, takes the place of the handling of invisible functions in the
theory-invariantevent has been modified so that the default action is an error rather than a warning.
+ Proof output that reports destructor elimination no longer uses the word ``generalizing''.
Again, please proceed to the subtopics for more thorough release notes.