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., FOO,
with a LAMBDA expression containing a free variable (a variable not among
in the LAMBDA formals). And, second, in one of the constraints being
instantiated there is a call of the function symbol FOO within the scope
of another 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
special variables.
Typographical errors were fixed in the documentation.