1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
|
<html>
<head><title>NOTE-2-0.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>NOTE-2-0</h2>ACL2 Version 2.0 (July, 1997) Notes
<pre>Major Section: <a href="RELEASE-NOTES.html">RELEASE-NOTES</a>
</pre><p>
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.<p>
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., <code>FOO</code>,
with a <code>LAMBDA</code> expression containing a free variable (a variable not among
in the <code>LAMBDA</code> formals). And, second, in one of the constraints being
instantiated there is a call of the function symbol <code>FOO</code> within the scope
of another <code>LAMBDA</code> expression. Unless you used such a functional
substitution, this bug fix will not affect you.<p>
<p>
Less important notes:<p>
The implementation of <code>PRINC$</code> was changed so that it was no longer
sensitive to the external setting of <code>*print-base*</code> and other Common Lisp
special variables.<p>
Typographical errors were fixed in the documentation.<p>
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
