ACL2 Version 1.8 (Summer, 1995) Notes
ACL2 can now use Ordered Binary Decision Diagram technology. See
bdd. There is also a proof-builder 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 (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 (<= 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.