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
36
37
38
39
40
41
42
43
44
45
46
47
48
49
|
<html>
<head><title>NOTE-2-4.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>NOTE-2-4</h2>ACL2 Version 2.4 (August, 1999) Notes
<pre>Major Section: <a href="RELEASE-NOTES.html">RELEASE-NOTES</a>
</pre><p>
Important changes: <p>
We corrected a soundness bug in Version 2.3 related to the handling of
<code><a href="IMMEDIATE-FORCE-MODEP.html">immediate-force-modep</a></code>. The bad behavior was noticed by Robert
Krug. Thanks!<p>
We corrected a bug that permitted <code><a href="VERIFY-GUARDS.html">verify-guards</a></code> to accept a function
even though a subfunction had not yet had its guards verified. Thanks to
John Cowles for noticing this.<p>
User defined single-threaded objects are now supported. See <a href="STOBJ.html">stobj</a>.
<p>
Less important notes:<p>
We corrected a bug that prevented the intended expansion of some recursive
function calls.<p>
We changed the handling of the primitive function <code><a href="ILLEGAL.html">ILLEGAL</a></code>, which
is logically defined to be <code>nil</code> but which is programmed to signal an
error, so that when it is evaluated as part of a proof, it does not signal
an error. The old handling of the function prevented some guard proofs
involving <code><a href="THE.html">THE</a></code> or <code><a href="LET.html">LET</a></code>s with internal declarations.<p>
We corrected a bug that permitted some <code>LOCAL</code> <code>DEFAXIOM</code> events to slip
into certified books.<p>
We corrected a bug that prevented the correct undoing of certain <code>DEFPKG</code>
forms.<p>
Changes were made to support CMU Lisp. Pete Manolios helped with these
changes.<p>
Changes were made to make the make files more compatible with Allegro
Common Lisp. Jun Sawada, who has been a great help with keeping ACL2
up and running at UT on various platforms, was especially helpful.
Thanks Jun.<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>
|
