Major Section: RELEASE-NOTES
A new key has been implemented for the
:ignore-ok. See set-ignore-ok.
It is now legal to have color events, such as
(red), in the
portcullis of a book. More generally, it is legal to set the
acl2-defaults-table in the portcullis of a book. For example, if
:red and then certify a book, the event
(red) will show
up in the portcullis of that book, and hence the definitions in that
book will all be red (except when overridden by appropriate
declarations or events). When that book is included, then as
always, its portcullis must first be ``raised,'' and that will cause
the default color to become red before the events in the book are
executed. As always, the value of
after execution of an
form will be the same as it was immediately before execution (and
hence, so will the default color). See portcullis and, for
more about books, see books.
ground-zero has been defined to contain exactly those rules
that are enabled when Acl2 starts up. See ground-zero.
nth is now enabled, correcting an oversight from
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,
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
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.
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.
set-irrelevant-formals-ok are now embedded
good-bye may now be used to quit entirely out of Lisp,
thus losing your work forever. This command works in akcl but may
not work in every Common Lisp.
ground-zero has been added that contains exactly the
enabled rules in the startup theory. See ground-zero.
define-pc-atomic-macro now automatically define
:red functions. (It used to be necessary, in general, to change
:red before invoking these.)
For a proof of the well-foundedness of
e0-ord-< on the
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
symbol-name-intern has been
modified. The definition of
firstn has been changed.
now defined. The definition of
integer-length has been modified.
The left-hand side of the rewrite rule
rational-implies2 has been
(* (numerator x) (/ (denominator x))) to
(* (/ (denominator x)) (numerator x)), in order to respect the
unary-/ is invisible with respect to
The `preprocess' process in the waterfall (see hints for a
discussion of the
:do-not hint) has been changed so that it works to
avoid case-splitting. The `simplify' process refuses to force
(see force) when there are
if terms, including
terms, in the goal being simplified.
apply is no longer introduced automatically by
translation of user input to internal form when functions are called
on inappropriate explicit values, e.g.,
The choice of which variable to use as the measured variable in a recursive definition has been very slightly changed.