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
50
51
52
53
54
55
56
57
58
59
60
61
62
|
<html>
<head><title>NOTE8-UPDATE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>NOTE8-UPDATE</h2>ACL2 Version 1.8 (Summer, 1995) Notes
<pre>Major Section: <a href="RELEASE-NOTES.html">RELEASE-NOTES</a>
</pre><p>
ACL2 can now use Ordered Binary Decision Diagram technology.
See <a href="BDD.html">bdd</a>. There is also a <a href="PROOF-CHECKER.html">proof-checker</a> <code>bdd</code> command.<p>
ACL2 is now more respectful of the intention of the function
<code><a href="HIDE.html">hide</a></code>. In particular, it is more careful not to dive inside any
call of <code><a href="HIDE.html">hide</a></code> during equality substitution and case splitting.<p>
The <code><a href="LD.html">ld</a></code> special (see <a href="LD.html">ld</a>) <code><a href="LD-PRE-EVAL-PRINT.html">ld-pre-eval-print</a></code> may now be used
to turn off printing of input forms during processing of
<code><a href="ENCAPSULATE.html">encapsulate</a></code> and <code><a href="CERTIFY-BOOK.html">certify-book</a></code> forms, by setting it to the value
<code>:never</code>, i.e., <code>(set-ld-pre-eval-print :never state)</code>.
See <a href="LD-PRE-EVAL-PRINT.html">ld-pre-eval-print</a>.<p>
The TUTORIAL documentation section has, with much help from Bill
Young, been substantially improved to a bona fide introduction, and
has been renamed <a href="ACL2-TUTORIAL.html">acl2-tutorial</a>.<p>
The term pretty-printer has been modified to introduce <code>(<= X Y)</code>
as an abbreviation for <code>(not (< Y X))</code>.<p>
Forward chaining and linear arithmetic now both benefit from the
evaluation of ground subterms.<p>
A new macro <code><a href="SET-INHIBIT-OUTPUT-LST.html">set-inhibit-output-lst</a></code> has been defined. This should
be used when setting the <a href="STATE.html">state</a> global <code>inhibit-output-lst</code>;
see <a href="SET-INHIBIT-OUTPUT-LST.html">set-inhibit-output-lst</a> and see <a href="PROOF-TREE.html">proof-tree</a>.<p>
The test for redundancy in definitions includes the <a href="GUARD.html">guard</a> and type
declarations. See <a href="REDUNDANT-EVENTS.html">redundant-events</a>.<p>
See <a href="GENERALIZED-BOOLEANS.html">generalized-booleans</a> for a discussion of a potential
soundness problem for ACL2 related to the question: Which Common
Lisp functions are known to return Boolean values?<p>
<p>
Here we will put some less important changes, additions, and so on.<p>
A bug has been fixed so that now, execution of <code>:comp t</code>
(see <a href="COMP.html">comp</a>) correctly handles non-standard characters.<p>
A bug in <code><a href="DIGIT-CHAR-P.html">digit-char-p</a></code> has been fixed, so that the ``default'' is
<code>nil</code> rather than <code>0</code>.<p>
<code><a href="TRUE-LISTP.html">True-listp</a></code> now tests the final <code><a href="CDR.html">cdr</a></code> against <code>nil</code> using <code><a href="EQ.html">eq</a></code>
instead of <code><a href="EQUAL.html">equal</a></code>, for improved efficiency. The logical meaning
is, however, unchanged.<p>
<code><a href="PUT-ASSOC-EQUAL.html">Put-assoc-equal</a></code> has been added to the logic (it used to have
<code>:</code><code><a href="DEFUN-MODE.html">defun-mode</a></code> <code>:</code><code><a href="PROGRAM.html">program</a></code>, and has been documented.<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>
|
