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
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
<html>
<head><title>NOTE-2-6-RULES.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>NOTE-2-6-RULES</h3>ACL2 Version 2.6 Notes on Changes in Rules and Constants
<pre>Major Section: <a href="NOTE-2-6.html">NOTE-2-6</a>
</pre><p>
The following symbols have been added to the list constant
<code>*common-lisp-specials-and-constants*</code>: <code>REPLACE</code>, <code>FILL</code>, <code>CHARACTER</code>,
<code>=</code>, <code>BREAK</code>, and <code>PRIN1</code>. This was done in support of ports to
Allegro 6.0 and Windows platforms (see <a href="NOTE-2-6-NEW-FUNCTIONALITY.html">note-2-6-new-functionality</a>).<p>
The list of symbols in <code>*acl2-exports*</code> has been modified, for
example to include <code>show-accumulated-persistence</code> and the legal
arguments to <code><a href="SET-INHIBIT-OUTPUT-LST.html">set-inhibit-output-lst</a></code>.<p>
Functions <code><a href="ZP.html">zp</a></code> and <code><a href="ZIP.html">zip</a></code> are now handled slightly differently. They are
are now disabled, but each comes with a <code>:</code><code><a href="REWRITE.html">rewrite</a></code> rule that allows
their expansion on non-variable terms, and also with a
<code>:</code><code><a href="COMPOUND-RECOGNIZER.html">compound-recognizer</a></code> rule that avoids the need for opening up these
functions when applied to variables. The resulting behavior should
be very similar to the behavior of previous versions, except that
case splits will be avoided when these functions are applied to
variables.<p>
Function <code><a href="STANDARD-STRING-ALISTP.html">standard-string-alistp</a></code> replaces function
<code>string-alistp</code>. For further discussion, see <a href="NOTE-2-6-GUARDS.html">note-2-6-guards</a>.<p>
Rules of class <code>:</code><code><a href="REWRITE.html">rewrite</a></code> whose conclusion is a term of the form
<code>(equal lhs rhs)</code> have always been stored in the expected way: <code>lhs</code>
rewrites to <code>rhs</code>. This way of storing <code>:rewrite</code> rules has been
extended to allow <code><a href="=.html">=</a></code>, <code><a href="EQ.html">eq</a></code>, or <code><a href="EQL.html">eql</a></code> in place of <code><a href="EQUAL.html">equal</a></code>.<p>
Rewrite rule <code>nth-update-nth</code>, in source file <code>axioms.lisp</code>, has been
strengthened.<p>
A new rewrite rule <code>equal-constant-+</code> has been added to the book
<code>arithmetic/equalities</code>. This should generally be a beneficial
change, but existing proofs involving the arithmetic books could
conceivably be affected.<p>
Function <code><a href="SYMBOL-PACKAGE-NAME.html">symbol-package-name</a></code> and constant <code>*main-lisp-package-name*</code>
have undergone small changes. This change should rarely be noticed
by users and is discussed elsewhere; see <a href="NOTE-2-6-SYSTEM.html">note-2-6-system</a>.<p>
We mention here that proofs involving <a href="STOBJ.html">stobj</a>s may need to be modified
because of changes in auxiliary functions generated by <code><a href="DEFSTOBJ.html">defstobj</a></code>.
(These changes were made in support of a new resizing capability,
mentioned elsewhere in these release notes;
see <a href="NOTE-2-6-NEW-FUNCTIONALITY.html">note-2-6-new-functionality</a>.<p>
In the distributed book directory <code>books/arithmetic/</code>, the book
<code>rationals-with-axioms-proved.lisp</code> has been renamed <code>rationals.lisp</code>.<p>
(ACL2(r) only) Rewrite rules <code>realp-+</code>, <code>realp-*</code>, <code>realp-unary--</code>, and
<code>realp-unary-/</code> have been added in analogy to existing rules
<code>rationalp-+</code>, <code>rationalp-*</code>, <code>rationalp-unary--</code>, and <code>rationalp-unary-/</code>.
Thanks to Jun Sawada for suggesting this change.<p>
The definition of <code><a href="AREF1.html">aref1</a></code> has been modified slightly. Previously, if
<code>*my-a*</code> were an array then <code>(aref1 'some-name *my-a* :header)</code> would
evaluate to the <code>cdr</code> of the <code><a href="HEADER.html">header</a></code> of <code>*my-a*</code> rather than to its
<code><a href="DEFAULT.html">default</a></code>. See <a href="ARRAYS.html">arrays</a>.<p>
Changes have been made in the <code>ihs</code> books, based on suggestions from
Jun Sawada, that support its use with ACL2(r) (see <a href="REAL.html">real</a>). The
primary change is to replace calls of <code><a href="RATIONALP.html">rationalp</a></code> with calls of
<code><a href="REAL_slash_RATIONALP.html">real/rationalp</a></code>, which should have no effect on users of standard
ACL2.<p>
<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>
|
