Acl2 Version 1.6 Notes
A new key has been implemented for the ACL2-defaults-table,
It is now legal to have color events, such as
A theory ground-zero has been defined to contain exactly those rules that are enabled when Acl2 starts up. See ground-zero.
The function nth is now enabled, correcting an oversight from Version 1.5.
Customization files no longer need to meet the syntactic restrictions put on books; rather, they can contain arbitrary Acl2 forms. See ACL2-customization.
Structured directory names and structured file names are supported; see especially the documentation for pathname, book-name, and cbd.
Acl2 now works with some Common Lisp implementations other than akcl, including Lucid, Allegro, and MCL.
A facility has been added for displaying proof trees, especially using emacs; see proof-tree.
There is a considerable amount of new documentation, in particular for the printing functions fmt, fmt1, and fms, and for the notion of Acl2 term (see term).
It is possible to introduce new well-founded relations, to specify which relation should be used by defun, and to set a default relation. See well-founded-relation-rule.
It is possible to make functions suggest new inductions. See induction.
It is possible to change how Acl2 expresses type-set information; in particular, this affects what clauses are proved when forced assumptions are generated. See type-set-inverter.
A new restriction has been added to defpkg, having to do with undoing. If you undo a defpkg 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 package-reincarnation-import-restrictions.
Theory-invariant and set-irrelevant-formals-ok are now embedded event forms.
A theory ground-zero has been added that contains exactly the enabled rules in the startup theory. See ground-zero.
For a proof of the well-foundedness of
Free variables are now handled properly for hypotheses of
When the system is loaded or saved, state is now bound to
Certify-book has been modified so that when it compiles a file, it loads that object file.
Defstub has been modified so that it works when the color is hot
Several basic, but not particularly commonly used, events have been
added or changed. The obscure axiom
The `preprocess' process in the waterfall (see hints for a
discussion of the
The choice of which variable to use as the measured variable in a recursive definition has been very slightly changed.