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
|
<html>
<head><title>NOTE-2-8-OTHER.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>NOTE-2-8-OTHER</h3>ACL2 Version 2.8 Notes on Miscellaneous Changes
<pre>Major Section: <a href="NOTE-2-8.html">NOTE-2-8</a>
</pre><p>
Execution of <code><a href="TABLE.html">table</a></code> events has been sped up in many cases by avoiding
excessive consing.<p>
ACL2 now warns if <code>:</code><code><a href="REWRITE.html">rewrite</a></code> (or <code>:</code><code><a href="DEFINITION.html">definition</a></code>) rules contain
free variables on the right-hand side. Thanks to Dave Greve for raising this
issue.<p>
Emacs file <code>emacs/emacs-acl2.el</code> has been updated to better comprehend the
notion of the ``ACL2 shell'', which is the buffer to which ACL2 forms are
written by commands defined in the above file. Thus, command <code>control-t e</code>
has been modified always to write to the ACL2 shell (which is <code>"*shell*"</code>
by default), and the following new commands have been defined.
<blockquote>
o control-t c<br>
Set the ACL2 shell to the current buffer.
o control-t b<br>
Change to the ACL2 shell.
</blockquote>
<p>
The commands <code>:</code><code><a href="PL.html">pl</a></code> and <code>:</code><code><a href="PR.html">pr</a></code> may now be given a macro name
that corresponds via the <code>macro-aliases-table</code> to a function name, so that
for example <code>:pl append</code> is treated the same as <code>:pl binary-append</code>. A
more interesting improvement, for <code>:pl</code> only, is that <code>:pl</code> may now take
any term. When <code>:pl</code> is given a term other than a symbol, it will print
all rewrite rules that match that term. Thanks to David Russinoff, Robert
Krug, and Bill Legato for getting this going.<p>
A new function, <code><a href="PKG-WITNESS.html">pkg-witness</a></code>, returns a symbol in the given package.<p>
The installation instructions have been updated, for example to give more
guidance on obtaining Lisp implementations and to mention the acl2-help
mailing list.<p>
Jared Davis has suggested some symbols to be added to <code>*acl2-exports*</code>,
and we have done so. Thanks, Jared.
<blockquote>
o <code>MFC</code> (used in <code><a href="SYNTAXP.html">syntaxp</a></code> and <code><a href="EXTENDED-METAFUNCTIONS.html">extended-metafunctions</a></code>; thanks
also to Robert Krug for this one)
o <code>ID</code>, <code>CLAUSE</code>, <code>WORLD</code>, and <code>STABLE-UNDER-SIMPLIFICATIONP</code> (used
in <code><a href="COMPUTED-HINTS.html">computed-hints</a></code>)
o <code><a href="SET-DEFAULT-HINTS.html">SET-DEFAULT-HINTS</a></code>
</blockquote>
<p>
The command <code>:</code><code><a href="PE.html">pe</a></code> has been improved so that when the event is inside
an included book, the path of included books (from the top-level book down to
the one containing the event) is shown. Thanks to Eric Smith (perhaps among
others) for pointing out the utility of this improvement.<p>
A new release of the rtl library has been included: <code>books/rtl/rel4/</code>.
See the <code>README</code> file in that directory.<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>
|
