Major Section: RELEASE-NOTES
This is the first version of ACL2 released under the copyright of the University of Texas (UT). Future releases of ACL2 will be made from UT rather than Computational Logic, Inc. (CLI). Version 2.0 is just Version 1.9 as released by CLI, with a few bugs fixed.
A bug causing an infinite loop was fixed in functional instantiation.
The bug manifested itself when two conditions occurred simultaneously:
First, the functional substitution replaces a function symbol, e.g.,
LAMBDA expression containing a free variable (a variable not among
LAMBDA formals). And, second, in one of the constraints being
instantiated there is a call of the function symbol
FOO within the scope
LAMBDA expression. Unless you used such a functional
substitution, this bug fix will not affect you.
Less important notes:
The implementation of
PRINC$ was changed so that it was no longer
sensitive to the external setting of
*print-base* and other Common Lisp
Typographical errors were fixed in the documentation.