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
|
<html>
<head><title>NOTE-2-7-RULES.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>NOTE-2-7-RULES</h3>ACL2 Version 2.7 Notes on Changes in Rules and Constants
<pre>Major Section: <a href="NOTE-2-7.html">NOTE-2-7</a>
</pre><p>
The <code><a href="DEFCONG.html">defcong</a></code> macro has been slightly changed. The difference is that
the variable generated with suffix <code>-EQUIV</code> will now be in the same package
as the name of the variable from which it is generated, rather than always
belonging to the ACL2 package. Thanks to Hanbing Liu for suggesting this
change. (Note that a couple of books have been modified to accommodate this
change, e.g., <code>books/finite-set-theory/set-theory</code>.)<p>
In Version_2.6, a change was made for rules of class <code>:</code><code><a href="REWRITE.html">rewrite</a></code> whose
conclusion is a term of the form <code>(EQV lhs rhs)</code>, where <code>EQV</code> is <code><a href="=.html">=</a></code>,
<code><a href="EQ.html">eq</a></code>, or <code><a href="EQL.html">eql</a></code>: the rule was stored as though <code>EQV</code> were
<code><a href="EQUAL.html">equal</a></code>. (See <a href="NOTE-2-6-RULES.html">note-2-6-rules</a>.) This change has been extended to rules
of class <code>:</code><code><a href="DEFINITION.html">definition</a></code>.<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>
|
