Major Section: RELEASE-NOTES
ACL2 can now use Ordered Binary Decision Diagram technology.
See bdd. There is also a proof-checker bdd command.
ACL2 is now more respectful of the intention of the function
hide. In particular, it is more careful not to dive inside any
call of hide during equality substitution and case splitting.
The ld special (see ld) ld-pre-eval-print may now be used
to turn off printing of input forms during processing of
encapsulate and certify-book forms, by setting it to the value
:never, i.e., (set-ld-pre-eval-print :never state).
See ld-pre-eval-print.
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 inhibit-output-lst;
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 :comp t
(see comp) correctly handles non-standard characters.
A bug in digit-char-p has been fixed, so that the ``default'' is
nil rather than 0.
True-listp now tests the final cdr against nil using eq
instead of equal, for improved efficiency. The logical meaning
is, however, unchanged.
Put-assoc-equal has been added to the logic (it used to have
:defun-mode :program, and has been documented.