Major Section: RELEASE-NOTES
By default, when the system is started it is illegal to use the
variable STATE 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
:set-state-ok tor, equivalently,
(set-state-ok t)to switch back to the old default mode. See set-state-ok
Set-state-ok is an event that affects the ACL2 defaults table
(see acl2-defaults-table). Recall that when books are
included, the defaults table is restored to its pre-inclusion state.
Thus, while a set-state-ok form will permit the book to define a
state-using function, it will not permit the user of the book to
make such a definition. We recommend putting (set-state-ok t) in
any book that defines a state using function.
Books certified under Version 1.8 must be recertified under Version 1.9. See :DOC version.
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 :HINTS require you to refer to clauses by
their exact name (see goal-spec) and because the new simplifier
proves more clauses than before, the goals produced have different
names. Thus, if a script uses :HINTS 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.
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 built-in-clauses
Wormholes can now be used in :logic mode functions. See wormhole
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 computed-hints and the extraordinarily long example in see using-computed-hints.
Hide terms may be rewritten with :rewrite rules about hide.
See hide, where we also now explain why hide terms are sometimes
introduced into your proof attempts.
A bug that sometimes caused the ``non-lazy IF'' hard error message was fixed.
A bug that sometimes caused a hard error in forward chaining was fixed.
A bug in print-rules (:pr) was fixed.
We report the use of :executable-counterparts in the evaluation of SYNTAXP forms.
Some documentation errors were fixed.
A bug in parent-tree tracking in add-literal-and-pt was fixed.
A bug in ok$, go$ and eval$ was fixed.
Clausify now optimizes (mv-nth 'k (list x0 ... xk ... xn)) to xk.