ACL2 Version 1.9 (Fall, 1996) 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
to switch back to the old default mode. See set-state-ok
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
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-clause
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.
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.