ACL2 Version 1.8 (Summer, 1995) Notes
ACL2 can now use Ordered Binary Decision Diagram technology. See
bdd. There is also a proof-builder
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
The TUTORIAL documentation section (now obsolete) has, with much help from Bill Young, been substantially improved to a bona fide introduction.
The term pretty-printer has been modified to introduce
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
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
A bug in digit-char-p has been fixed, so that the ``default'' is
True-listp now tests the final cdr against
Put-assoc-equal has been added to the logic (it used to have