NOTE9

ACL2 Version 1.9 (Fall, 1996) Notes
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 t
or, 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.