Major Section: RELEASE-NOTES
ACL2 can now use Ordered Binary Decision Diagram technology.
See bdd. There is also a proof-checker
ACL2 is now more respectful of the intention of the function
hide. In particular, it is more careful not to dive inside any
hide during equality substitution and case splitting.
ld special (see ld)
ld-pre-eval-print may now be used
to turn off printing of input forms during processing of
certify-book forms, by setting it to the value
(set-ld-pre-eval-print :never state).
The TUTORIAL documentation section has, with much help from Bill Young, been substantially improved to a bona fide introduction, and has been renamed acl2-tutorial.
The term pretty-printer has been modified to introduce
(<= X Y)
as an abbreviation for
(not (< Y X)).
Forward chaining and linear arithmetic now both benefit from the evaluation of ground subterms.
A new macro
set-inhibit-output-lst has been defined. This should
be used when setting the state global
see set-inhibit-output-lst and see proof-tree.
The test for redundancy in definitions includes the guard and type declarations. See redundant-events.
See generalized-booleans for a discussion of a potential soundness problem for ACL2 related to the question: Which Common Lisp functions are known to return Boolean values?
Here we will put some less important changes, additions, and so on.
A bug has been fixed so that now, execution of
(see comp) correctly handles non-standard characters.
A bug in
digit-char-p has been fixed, so that the ``default'' is
nil rather than
True-listp now tests the final
equal, for improved efficiency. The logical meaning
is, however, unchanged.
Put-assoc-equal has been added to the logic (it used to have
program, and has been documented.