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
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
<html>
<head><title>NOTE6.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>NOTE6</h2>Acl2 Version 1.6 Notes
<pre>Major Section: <a href="RELEASE-NOTES.html">RELEASE-NOTES</a>
</pre><p>
A new key has been implemented for the <code><a href="ACL2-DEFAULTS-TABLE.html">acl2-defaults-table</a></code>,
<code>:ignore-ok</code>. See <a href="SET-IGNORE-OK.html">set-ignore-ok</a>.<p>
It is now legal to have color <a href="EVENTS.html">events</a>, such as <code>(red)</code>, in the
<a href="PORTCULLIS.html">portcullis</a> of a book. More generally, it is legal to set the
<code><a href="ACL2-DEFAULTS-TABLE.html">acl2-defaults-table</a></code> in the <a href="PORTCULLIS.html">portcullis</a> of a book. For example, if
you execute <code>:red</code> and then certify a book, the event <code>(red)</code> will show
up in the <a href="PORTCULLIS.html">portcullis</a> of that book, and hence the definitions in that
book will all be red (except when overridden by appropriate
declarations or <a href="EVENTS.html">events</a>). When that book is included, then as
always, its <a href="PORTCULLIS.html">portcullis</a> must first be ``raised,'' and that will cause
the default color to become red before the <a href="EVENTS.html">events</a> in the book are
executed. As always, the value of <code><a href="ACL2-DEFAULTS-TABLE.html">acl2-defaults-table</a></code> immediately
after execution of an <code><a href="INCLUDE-BOOK.html">include-book</a></code>, <code><a href="CERTIFY-BOOK.html">certify-book</a></code>, or <code><a href="ENCAPSULATE.html">encapsulate</a></code>
form will be the same as it was immediately before execution (and
hence, so will the default color). See <a href="PORTCULLIS.html">portcullis</a> and, for
more about books, see <a href="BOOKS.html">books</a>.<p>
A theory <code><a href="GROUND-ZERO.html">ground-zero</a></code> has been defined to contain exactly those rules
that are <a href="ENABLE.html">enable</a>d when Acl2 starts up. See <a href="GROUND-ZERO.html">ground-zero</a>.<p>
The function <code><a href="NTH.html">nth</a></code> is now <a href="ENABLE.html">enable</a>d, correcting an oversight from
Version 1.5.<p>
Customization files no longer need to meet the syntactic
restrictions put on <a href="BOOKS.html">books</a>; rather, they can contain arbitrary Acl2
forms. See <a href="ACL2-CUSTOMIZATION.html">acl2-customization</a>.<p>
Structured directory names and structured file names are supported;
see especially the documentation for <a href="PATHNAME.html">pathname</a>, <a href="BOOK-NAME.html">book-name</a>,
and <code><a href="CBD.html">cbd</a></code>.<p>
Acl2 now works with some Common Lisp implementations other than
akcl, including Lucid, Allegro, and MCL.<p>
A facility has been added for displaying proof trees, especially
using emacs; see <a href="PROOF-TREE.html">proof-tree</a>.<p>
There is a considerable amount of new <a href="DOCUMENTATION.html">documentation</a>, in particular
for the printing functions <code><a href="FMT.html">fmt</a></code>, <code><a href="FMT1.html">fmt1</a></code>, and <code><a href="FMS.html">fms</a></code>, and for the notion of
Acl2 term (see <a href="TERM.html">term</a>).<p>
It is possible to introduce new well-founded relations, to specify
which relation should be used by <code><a href="DEFUN.html">defun</a></code>, and to set a default
relation. See <a href="WELL-FOUNDED-RELATION.html">well-founded-relation</a>.<p>
It is possible to make functions suggest new inductions.
See <a href="INDUCTION.html">induction</a>.<p>
It is possible to change how Acl2 expresses <a href="TYPE-SET.html">type-set</a> information; in
particular, this affects what clauses are proved when <a href="FORCE.html">force</a>d
assumptions are generated. See <a href="TYPE-SET-INVERTER.html">type-set-inverter</a>.<p>
A new restriction has been added to <code><a href="DEFPKG.html">defpkg</a></code>, having to do with
undoing. If you undo a <code><a href="DEFPKG.html">defpkg</a></code> and define the same package name
again, the imports list must be identical to the previous imports or
else an explanatory error will occur.
See <a href="PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS.html">package-reincarnation-import-restrictions</a>.<p>
<code><a href="THEORY-INVARIANT.html">Theory-invariant</a></code> and <code><a href="SET-IRRELEVANT-FORMALS-OK.html">set-irrelevant-formals-ok</a></code> are now embedded
event forms.<p>
The command <code>:</code><code><a href="GOOD-BYE.html">good-bye</a></code> may now be used to quit entirely out of Lisp,
thus losing your work forever. This command works in akcl but may
not work in every Common Lisp.<p>
A theory <code><a href="GROUND-ZERO.html">ground-zero</a></code> has been added that contains exactly the
<a href="ENABLE.html">enable</a>d rules in the <a href="STARTUP.html">startup</a> theory. See <a href="GROUND-ZERO.html">ground-zero</a>.<p>
<code>Define-pc-macro</code> and <code>define-pc-atomic-macro</code> now automatically define
<code>:red</code> functions. (It used to be necessary, in general, to change
color to <code>:red</code> before invoking these.)<p>
<p>
For a proof of the well-foundedness of <code>e0-ord-<</code> on the <code>e0-ordinalp</code>s,
see <a href="PROOF-OF-WELL-FOUNDEDNESS.html">proof-of-well-foundedness</a>. [Note added later: Starting with
Version_2.8, <code><a href="O_lt_.html">o<</a></code> and <code><a href="O-P.html">o-p</a></code> replace <code>e0-ord-<</code> and <code>e0-ordinalp</code>,
respectively.]<p>
Free variables are now handled properly for hypotheses of
<code>:</code><code><a href="TYPE-PRESCRIPTION.html">type-prescription</a></code> rules.<p>
When the system is loaded or saved, <code><a href="STATE.html">state</a></code> is now bound to
<code>*the-live-state*</code>.<p>
<code><a href="CERTIFY-BOOK.html">Certify-book</a></code> has been modified so that when it compiles a file, it
loads that object file.<p>
<code><a href="DEFSTUB.html">Defstub</a></code> has been modified so that it works when the color is hot
(<code>:red</code> or <code>:pink</code>).<p>
Several basic, but not particularly commonly used, <a href="EVENTS.html">events</a> have been
added or changed. The obscure axiom <code>symbol-name-intern</code> has been
modified. The definition of <code>firstn</code> has been changed. <code><a href="BUTLAST.html">Butlast</a></code> is
now defined. The definition of <code><a href="INTEGER-LENGTH.html">integer-length</a></code> has been modified.
The left-hand side of the rewrite rule <code>rational-implies2</code> has been
changed from <code>(* (numerator x) (/ (denominator x)))</code> to
<code>(* (/ (denominator x)) (numerator x))</code>, in order to respect the
fact that <code><a href="UNARY-_slash_.html">unary-/</a></code> is invisible with respect to <code><a href="BINARY-_star_.html">binary-*</a></code>.
See <a href="LOOP-STOPPER.html">loop-stopper</a>.<p>
The `preprocess' process in the waterfall (see <a href="HINTS.html">hints</a> for a
discussion of the <code>:do-not</code> hint) has been changed so that it works to
avoid case-splitting. The `simplify' process refuses to force
(see <a href="FORCE.html">force</a>) when there are <code><a href="IF.html">if</a></code> terms, including <code><a href="AND.html">and</a></code> and <code><a href="OR.html">or</a></code>
terms, in the goal being simplified.<p>
The function <code>apply</code> is no longer introduced automatically by
translation of user input to internal form when functions are called
on inappropriate explicit values, e.g., <code>(car 3)</code>.<p>
The choice of which variable to use as the measured variable in a
recursive definition has been very slightly changed.<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>
|
