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
|
<html>
<head><title>NOTE9.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>NOTE9</h2>ACL2 Version 1.9 (Fall, 1996) Notes
<pre>Major Section: <a href="RELEASE-NOTES.html">RELEASE-NOTES</a>
</pre><p>
By default, when the system is started it is illegal to use the
variable <code><a href="STATE.html">STATE</a></code> as a formal parameter of a function definition.
The aim is to prevent novice users from stumbling into the Byzantine
syntactic restrictions on that variable symbol. Use
<pre>
:set-state-ok t
</pre>
or, equivalently,
<pre>
(set-state-ok t)
</pre>
to switch back to the old default mode. See <a href="SET-STATE-OK.html">set-state-ok</a><p>
<code>Set-state-ok</code> is an event that affects the ACL2 defaults table
(see <a href="ACL2-DEFAULTS-TABLE.html">acl2-defaults-table</a>). Recall that when books are
included, the defaults table is restored to its pre-inclusion state.
Thus, while a <code>set-state-ok</code> form will permit the book to define a
<code>state</code>-using function, it will not permit the user of the book to
make such a definition. We recommend putting <code>(set-state-ok t)</code> in
any book that defines a <code>state</code> using function.<p>
Books certified under Version 1.8 must be recertified under Version
1.9. See :DOC version.<p>
The simplifier has been made to look out for built-in clauses,
whereas in past versions such clauses were only noticed by the
``preprocessor'' at the top of the waterfall. THIS CHANGE MAY
PREVENT OLD SCRIPTS FROM REPLAYING! The undesirable side-effect is
caused by the fact that <code>:HINTS</code> require you to refer to clauses by
their exact name (see <a href="GOAL-SPEC.html">goal-spec</a>) and because the new simplifier
proves more clauses than before, the goals produced have different
names. Thus, if a script uses <code>:HINTS</code> that refer to clauses other
than "Goal", e.g., "Subgoal 1.3" then the hint may be applied to
a different subgoal than originally intended.<p>
The use of built-in-clauses has been made more efficient. If a set
of clauses arise often in a piece of work, it might be advantageous
to build them in even if that results in a large set (hundreds?) of
built-in clauses. See <a href="BUILT-IN-CLAUSES.html">built-in-clauses</a><p>
Wormholes can now be used in :logic mode functions. See <a href="WORMHOLE.html">wormhole</a><p>
It is now possible to provide ``computed hints.'' For example, have
you ever wished to say ``in all goals with a name like this, :use
that'' or ``if this term is in the subgoal, then :use that''? Well,
see <a href="COMPUTED-HINTS.html">computed-hints</a> and the extraordinarily long example in
see <a href="USING-COMPUTED-HINTS.html">using-computed-hints</a>.<p>
<code>Hide</code> terms may be rewritten with :rewrite rules about <code>hide</code>.
See <a href="HIDE.html">hide</a>, where we also now explain why <code>hide</code> terms are sometimes
introduced into your proof attempts.
<p>
A bug that sometimes caused the ``non-lazy IF'' hard error message
was fixed.<p>
A bug that sometimes caused a hard error in forward chaining was
fixed.<p>
A bug in print-rules (:pr) was fixed.<p>
We report the use of :executable-counterparts in the evaluation of
SYNTAXP forms.<p>
Some documentation errors were fixed.<p>
A bug in parent-tree tracking in add-literal-and-pt was fixed.<p>
A bug in ok$, go$ and eval$ was fixed.<p>
Clausify now optimizes (mv-nth 'k (list x0 ... xk ... xn)) to xk.<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>
|
