This is documentation for ACL2 Version 3.3
Copyright (C) 2007  University of Texas at Austin

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

Written by:  Matt Kaufmann and J Strother Moore
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188 U.S.A.

NOTE-3-3    ACL2 Version  3.3 (November, 2007) Notes

NOTE!  New users can ignore these release notes, because the
documentation has been updated to reflect all changes that are recorded
here.

Below we roughly organize the changes since Version  3.2.1 into new
features, bug fixes, prover algorithm enhancements, and miscellaneous.
Also see NOTE-3-2-1 for other changes since Version  3.2.

*NEW FEATURES*

A new "gag-mode" provides less verbose, more helpful feedback from the
theorem prover, in support of The Method (see THE-METHOD).  See
SET-GAG-MODE.  We recommend the use of gag-mode, which may
become the default in future ACL2 releases, and we welcome suggestions
for improvement.  We thank Robert Krug and Sandip Ray for helpful
feedback in the design of gag-mode.  Note that when proofs fail, then
even without gag-mode and even if proof output is inhibited, the
summary will contain a useful listing of so-called "key checkpoints"
(see SET-GAG-MODE).

Added support for a leading `~' in filenames.  Thanks to Bob Boyer for
suggesting this enhancement.  Note that since `~/' depends on the user,
it is disallowed in books to be certified (see CERTIFY-BOOK),
since otherwise an include-book form in a book, b, could have a
different meaning at certification time than at the time include-book
is later executed on book b.

Made a change to allow (time$ FORM) and (with-prover-time-limit TIME
FORM) when FORM includes make-event calls that change the ACL2 world.
Thanks to Jared Davis for requesting such support for time$.

Computed hints (see COMPUTED-HINTS) may now produce a so-called
"error triple", i.e., a result of the form (mv erp val state), where a
non-nil erp causes an error, and otherwise val is the value of the
hint.  It remains legal for a computed hint to return a single ordinary
value; indeed, the symbol form of a computed hint must still be a
function that returns an ordinary single value.

New hints provide additional control of the theorem prover, as follows.
See HINTS for more details, and see new distributed book
directory books/hints/ for examples, in particular file
basic-tests.lisp in that directory for simple examples.

     o The hint :OR (hints-1 ... hints-k) causes an attempt to prove the
     specified goal using each hints-i in turn, until the first of these
     succeeds.  If none succeeds, then the prover proceeds after
     heuristically choosing the "best" result, taking into account the
     goals pushed in each case for proof by induction.

     o A custom hint is a keyword that the user associates with a
     corresponding hint-generating function by invoking
     add-custom-keyword-hint.  Thus, a custom hint may be viewed as a
     convenient sort of computed hint.

     o A custom hint, :MERGE, is implemented in distributed book
     books/hints/merge.lisp.  It is useful for combining hints.

     o A sophisticated yet useful custom hint is the :CONSIDER hint
     implemented in distributed book books/hints/consider-hint.lisp.
     With this hint, you can for example give the equivalent of a :USE
     hint without the need to supply an instantiation.  Include that
     book in order to see documentation online with :doc consideration,
     and see the book books/hints/consider-hint-tests.lisp for examples.

A new hint, :reorder, allows the specification of which subgoals are to
be considered first.  Thanks to Sandip Ray for putting forward this
idea.

Enhanced set-saved-output by supporting a second argument of :same,
which avoids changing which output is inhibited.

Added macros thm? and not-thm? to distributed book
books/make-event/eval.lisp, so that it's easy to test within a certified
book that a proof attempt succeeds or that it fails.

Added printing function cw!, which is analogous to cw just as fmt! is
to fmt, i.e., printing so that the result can be read back in.  Thanks
to Jared Davis for suggesting this enhancement (after doing his own
implementation).

The ACL2 customization file can now be specified using environment
variable ACL2-CUSTOMIZATION.  See ACL2-CUSTOMIZATION.  Thanks
to Peter Dillinger for requesting this feature.

Added new emacs capabilities for proof trees (all documented in emacs):

     o New function start-proof-tree-noninteractive, for example
     (start-proof-tree-noninteractive "*shell*")

     o C-z o      Switch to another frame

     o C-z b      Switch to prooftree buffer

     o C-z B      Switch to prooftree buffer in "prooftree-frame" frame

Added Common Lisp function, search, as a macro in logic mode, with
limited support for keyword arguments.  Thanks to Warren Hunt for
requesting this addition.

Sandip Ray has contributed a book, books/make-event/defrefine.lisp, that
provides a collection of macros to aid in reasoning about ACL2
functions via refinement.

Wrote and incorporated new utility for listing all the theorems in an
included book.  See books/misc/book-thms.lisp.  Thanks to Jared Davis
for requesting this functionality.

The new distributed book misc/defp.lisp generalizes the defpun macro to
allow more general forms of tail recursion.

(Low-level printing improvement) A new function,
set-ppr-flat-right-margin, allows the right margin for certain kinds of
"flat" printing to exceed column 40.  Thanks to Jared Davis for pointing
out that state global variables 'fmt-hard-right-margin and
'fmt-soft-right-margin are not alone sufficient to extend the right
margin in all cases.

The event add-include-book-dir can now take a relative pathname as an
argument.  Formerly, it required an absolute pathname.

A new book, books/misc/defopener.lisp, provides a utility creating a
theorem that equates a term with its simplification.

ACL2 now provides limited support for the Common Lisp primitive FLET,
which supports local function bindings.  See FLET.  Thanks to
Warren Hunt for requesting this feature.

Added a definition of boole$, a close analogue of Common Lisp function
boole.  Thanks to Bob Boyer for providing an initial implementation.

*BUG FIXES*

Fixed defstobj to inhibit a potentially useless theory warning.

Fixed a bug in the application of certify-book to relative pathnames
for files in other than the current directory.  Thanks to Amr Helmy for
bringing this bug to our attention.

Fixed a bug in :pl and :pr for displaying rules of class :meta.  Thanks
to Jared Davis for finding this bug and providing a fix.

Formerly, set-default-backchain-limit was not a legal event form for
encapsulate forms and books.  This has been fixed.  Thanks to Robert
Krug and Sandip Ray for bringing this bug to our attention.

Fixed the handling of hints in proof-checker commands for the prover,
such as bash -- see PROOF-CHECKER-COMMANDS -- so that the user
can override the default settings of hints, in particular of :do-not
and :do-not-induct hints attached to "Goal".  This fix also applies to
the distributed book misc/bash.lisp, where Robert Krug noticed that he
got an error with :hints (("Goal" :do-not '(preprocess))); we thank
Robert for pointing out this problem.

Fixed a bug in handling of stobjs occurring in guards of functions whose
guards have been verified.  In such cases, a raw Lisp error was possible
when proving theorems about non-"live" stobjs.  We thank Daron Vroon
for sending us an example that highlighted this bug.  The following
(simpler) example causes such an error in previous versions of ACL2.

     (defstobj st fld)
     (defun foo (st)
       (declare (xargs :stobjs st :guard (fld st)))
       st)
     (thm (equal (foo '(3))
                 '(3)))

The dmr feature for dynamic monitoring of rewrites had a bug, where the
file used for communicating with emacs was the same for all users,
based on who built the ACL2 executable image.  This has been fixed.
Thanks to Robert Krug for bringing this bug to our attention.

Fixed a bug in some warnings, in particular the warning for including an
uncertified book, that was giving an incorrect warning summary string.

Inclusion of uncertified books erroneously re-used make-event
expansions that were stored in stale certificates.  This is no longer
the case.  Thanks to Jared Davis for bringing this bug to our attention.

Fixed a bug that was disallowing calls of with-output in events that
were executing before calling certify-book.

Modified the functionality of binop-table so binary function symbols
are properly supported (hence with no action based on right-associated
arguments).  See ADD-BINOP.

Fixed small proof-checker issues related to packages.  Emacs commands
ctrl-t d and ctrl-t ctrl-d now work properly with colon (`:') and
certain other punctuation characters.  The p-top command now prints
"***" regardless of the current package.

Fixed a bug that allowed certify-book to succeed without specifying
value t for keyword argument :skip-proofs-okp, even with include-book
events in the certification world depending on events executed under
skip-proofs.

Improved show-accumulated-persistence in the following two ways.
Thanks to Robert Krug for requesting these improvements and for
providing useful feedback.

     o It can provide more complete information when aborting a proof.

     o The :frames reported for a rule are categorized as "useful" and
     "useless" according to whether they support "useful" or "useless"
     :tries of that rule, respectively.  See
     ACCUMULATED-PERSISTENCE for further explanation.

Modified make-event so that the reported time and warnings include
those from the expansion phase.  In analogy with encapsulate and progn,
the rules reported still do not include those from subsidiary events
(including the expansion phase).  A related change to ld avoids
resetting summary information (time, warnings) with each top-level form
evaluation; events already handle this information themselves.

Fixed set-inhibit-output-lst so that all warnings are inhibited when
warning! but not warning is included in the list.  Formerly, only
soundness-related warnings were inhibited in this case.  Thanks to Eric
Smith for bringing this bug to our attention.

Distributed directory doc/HTML/ now again includes installation
instructions (which was missing in Version_3.2.1), in
doc/HTML/installation/installation.html.

Some fixes have been made for proof-tree support.

     o Proof-tree output is no longer inhibited automatically during
     certify-book, though it continues to be inhibited by default (i.e.,
     ACL2 continues to start up as though set-inhibit-output-lst has
     been called with argument '(proof-tree)).

     o Fixed a bug in Xemacs support for proof-tree help keys C-z h and
     C-z ?.

     o Fixed a bug in proof-trees that was failing to deal with the
     case that a goal pushed for proof by induction is subsumed by such
     a goal to be proved later.  Now, the proof-tree display regards
     such subsumed goals as proved, as is reported in the theorem
     prover's output.

Fixed a bug that was disallowing value-triple forms inside encapsulate
forms in a certification world (see PORTCULLIS).

If the :load-compiled-file argument of a call of include-book is :comp,
then an existing compiled file will be loaded, provided it is more
recent than the corresponding book (i.e., .lisp file).  A bug was
causing the compiled file to be deleted and then reconstructed in the
case of :comp, where this behavior was intended only for :comp!.

Fixed a bug that was avoiding compilation of some executable
counterparts (sometimes called "*1* functions") during certify-book,
and also during include-book with :load-compiled-file value of :comp or
:comp!).  Thanks to Eric Smith for sending a small example to bring this
bug to our attention.

Incorporated a fix from Eric Smith for a typo (source function
ancestors-check1) that could cause hard Lisp errors.  Thanks, Eric!

Fixed the following issues with packages and book certificates.  See
HIDDEN-DEATH-PACKAGE if you are generally interested in such
issues, and for associated examples, see comments on "Fixed the
following issues with packages" in note-3-3 in the ACL2 source code.

     o Reduced the size of .cert files by eliminating some unnecessary
     defpkg events generated for the portcullis.

     o Fixed a bug that has caused errors when reading symbols from a
     portcullis that are in undefined packages defined in locally
     included books.

     o Fixed a bug that could lead to failure of include-book caused by
     a subtle interaction between set-ignore-ok and defpkg events
     generated for the portcullis of a certificate.

*PROVER ALGORITHM ENHANCEMENTS*

Non-linear arithmetic (see NON-LINEAR-ARITHMETIC) has been
improved to be more efficient or more powerful in some cases.  Thanks
to Robert Krug for contributing these improvements.

Improved certain (so-called "type-set") reasoning about whether or not
expressions denote integers.  Thanks to Robert Krug for contributing
code to implement this change, along with examples illustrating its
power that are now distributed in the book
books/misc/integer-type-set-test.lisp.

Improved ACL2's heuristics for relieving hypotheses, primarily to use
linear reasoning on conjuncts and disjuncts of the test of an if
expression.  For example, given a hypothesis of the form (if (or term1
term2) ...), ACL2 will now use linear reasoning to attempt to prove
both term1 and term2, not merely for term2.  Thanks to Robert Krug for
supplying examples illustrating the desirability of such an improvement
and for useful discussions about the fix.

Made a slight heuristic change, so that when a hypothesis with let or
mv-let subterms (i.e. lambda subterms) rewrites to t, then that
hypothesis is necessarily eliminated.  Thanks to Jared Davis for sending
an example that led us to develop this change, and thanks to Robert
Krug for a helpful discussion.

*MISCELLANEOUS*

Added documentation on how to use make-event to avoid duplicating
expensive computations, thanks to Jared Davis.  See
USING-TABLES-EFFICIENTLY.

Modified the error message for calls of undefined functions to show the
arguments.  Thanks to Bob Boyer for requesting this enhancement.

Modified utilies :pr, :pr!, :pl, and :show-bodies to incorporate code
contributed by Jared Davis.  That code defines low-level source
functions info-for-xxx that collect information about rules, which is
thus available to advanced users.

Dynamic monitoring of rewrites (see DMR) has been improved in
the following ways, as suggested by Robert Krug.

     o Some stale entries from the rewrite stack are no longer printed,
     in particular above ADD-POLYNOMIAL-INEQUALITIES.

     o An additional rewrite stack entry is made when entering
     non-linear arithmetic (see NON-LINEAR-ARITHMETIC).

     o An ADD-POLYNOMIAL-INEQUALITIES entry is printed with a counter,
     to show how often this process is called.

Modified save-exec so that the newly-saved image will have the same raw
Lisp package as the existing saved image.  This is a very technical
change that will likely not impact most users; for example, the package
in the ACL2 read-eval-print loop (see LP) had already persisted
from the original to newly-saved image.  Thanks to Jared Davis for
suggesting this change.

Changed make-event expansion so that changes to set-saved-output,
set-print-clause-ids, set-fmt-soft-right-margin, and
set-fmt-hard-right-margin will persist after being evaluated during
make-event expansion.  (Specifically, *protected-system-state-globals*
has been modified; see MAKE-EVENT-DETAILS.)  Thanks to Jared
Davis for bringing this issue to our attention.

Output from the proof-checker is now always enabled when invoking
verify, even if it is globally inhibited (see
SET-INHIBIT-OUTPUT-LST).

Improved the message printed when an :induct hint fails, to give more
information in some cases.  Thanks to Rex Page for suggesting where an
improvement could be made and providing useful feedback on an initial
improvement.

Added a warning for congruence rules (see DEFCONG) that specify
iff as the second equivalence relation when equal can be used instead.
Those who heed these warnings can eliminate certain subsequent
double-rewrite warnings for rewrite rules with conclusions of the form
(iff term1 term2), and hence implicitly for Boolean conclusions term1
that are interpreted as (iff term1 t).  Thanks to Sarah Weissman for
sending us an example that highlighted the need for such a warning.

Modified macro :redef! (which is for system implementors) so that it
eliminates untouchables.

Several improvements have been made to the experimental hons/memoization
version of ACL2.  See HONS-AND-MEMOIZATION.

The distributed books directory, (@ distributed-books-dir), is now
printed in the start-up message.

NOTE-3-3(R)    ACL2 Version  3.3(r) (xxx, 20xx) Notes

Please also see NOTE-3-3 for changes to Version  3.3 of ACL2.

NOTE1    Acl2 Version 1.1 Notes

The new features are extensively documented.  The relevant topics are:

Related topics other than immediate subtopics:

It is especially important to read all of of the documentation for
books before trying to use books.  However, the new :more keyword
command is so handy for reading long documentation strings that we
recommend you start with :doc more if reading at the terminal.  Some
documentation has been written for guards which you might find
interesting.

NOTE2    Acl2 Version 1.2 Notes

Hacker mode has been eliminated and programming mode has been added.
Programming mode is unsound but does syntax checking and permits
redefinitions of names.  See :doc load-mode and :doc g-mode.

The arguments to ld have changed.  Ld is now much more sophisticated.
See LD.

For those occasions on which you wish to look at a large list structure
that you are afraid to print, try (walkabout x state), where x is an
Acl2 expression that evaluates to the structure in question.  I am
afraid there is no documentation yet, but it is similar in spirit to
the Interlisp structure editor.  You are standing on an object and
commands move you around in it.  E.g., 1 moves you to its first
element, 2 to its second, etc.; 0 moves you up to its parent; nx and bk
move you to its next sibling and previous sibling; pp prettyprints it;
q exits returning nil; = exits returning the thing you're standing on;
(= symb) assigns the thing you're standing on to the state global
variable symb.

Several new hints have been implemented, including :by and :do-not.
The old :do-not-generalize has been scrapped in favor of such new hints
as :do-not (generalize elim).  :By lets you say "this goal is subsumed
by" a given lemma instance.  The :by hint also lets you say "this goal
can't be proved yet but skip it and see how the rest of the proof
goes." See HINTS.

NOTE3    Acl2 Version 1.3 Notes

Programming mode has been eliminated.  Instead, all functions have a
"color" which indicates what can be done with the function.  For
example, :red functions can be executed but have no axioms describing
them.  Thus, :red functions can be introduced after passing a simple
syntactic check and they can be redefined without undoing.  But nothing
of consequence can be proved about them.  At the other extreme are
:gold functions which can be executed and which also have passed both
the termination and the guard verification proofs.  The color of a
function can be specified with the new xargs keyword, :color, which, if
omitted defaults to the global setting of ld-color.  Ld-color replaces
load-mode.  Setting ld-color to :red causes behavior similar to the old
:g-mode.  Setting ld-color to :gold causes behavior similar to the old
:v-mode.  It is possible to prototype your system in :red and then
convert :red functions to :blue individually by calling
verify-termination on them.  They can then be converted to :gold with
verify-guards.  This allows us to undertake to verify the termination
and guards of system functions.  See :doc color for an introduction to
the use of colors.

Type prescription rules have been added.  Recall that in Nqthm, some
rewrite rules were actually stored as "type-prescriptions."  Such rules
allow the user to inform Nqthm's primitive type mechanism as to the
kinds of shells returned by a function.  Earlier versions of Acl2 did
not have an analogous kind of rule because Acl2's type mechanism is
complicated by guards.  Version 1.3 supports type-prescription rules.
See TYPE-PRESCRIPTION.

Three more new rule-classes implement congruence-based rewriting.  It
is possible to identify a binary relation as an equivalence relation
(see EQUIVALENCE), to show that one equivalence relation
refines another (see REFINEMENT) and to show that a given
equivalence relation is maintained when rewriting a given function
call, e.g., (fn ...xk...), by maintaining another equivalence relation
while rewriting the kth argument (see CONGRUENCE).  If r has
been shown to be an equivalence relation and then (implies hyps (r (foo
x) (bar x))) is proved as a :rewrite rule, then instances of (foo x)
will be replaced by corresponding instances of (bar x) provided the
instance occurs in a slot where the maintainence of r-equivalence is
known to be sufficient and hyps can be established as usual.

In Version 1.2, rule-classes were simple keywords, e.g., :rewrite or
:elim.  In Version 1.3, rule-classes have been elaborated to allow you
to specify how the theorem ought to be used as a rule.  That is, the
new rule-classes allows you to separate the mathematical statement of
the formula from its interpretation as a rule.  See
RULE-CLASSES.

Rules used to be named by symbols, e.g., car and car-cons were the
names of rules.  Unfortunately, this was ambiguous because there are
three rules associated with function symbols: the symbolic definition,
the executable counterpart, and the type-prescription; many different
rules might be associated with theorems, depending on the rule classes.
In Version 1.3 rules are named by "runes" (which is just short hand
for "rule names").  Example runes are (:definition car),
(:executable-counterpart car), and (:type-prescription car . 1).  Every
rule added by an event has a different name and you can enable and
disable them independently.  See RUNE and see THEORIES.

The identity function force, of one argument, has been added and given
a special interpretation by the functions responsible for establishing
hypotheses in backchaining: When the system fails to establish some
hypothesis of the form (force term), it simply assumes it is true and
goes on, delaying until later the establishment of term.  In
particular, pushes a new subgoal to prove term in the current context.
When that subgoal is attacked, all of the resources of the theorem
prover, not just rewriting, are brought to bear.  Thus, for example, if
you wish to prove the rule (implies (good-statep s) (equal (exec s n)
s')) and it is your expectation that every time exec appears its first
argument is a good-statep then you might write the rule as (implies
(force (good-statep s)) (equal (exec s n) s')).  This rule is
essentially an unconditional rewrite of (exec s n) to s' that spawns
the new goal (good-statep s).  See FORCE.  Because you can now
specify independently how a theorem is used as a rule, you need not
write the force in the actual theorem proved.  See RULE-CLASSES.

Version 1.3 supports a facility similar to Nqthm's break-lemma.  See
BREAK-REWRITE.  You can install "monitors" on runes that will
cause interactive breaks under certain conditions.

Acl2 also provides "wormholes" which allow you to write functions that
cause interaction with the user but which do not require that you have
access to state.  See WORMHOLE.

The rewriter now automatically backchains to stronger recognizers.
There is no user hook to this feature but it may simplify some proofs
with which older versions of Acl2 had trouble.  For example, if the
rewriter is trying to prove (rationalp (foo a b c)) it is now smart
enough to try lemmas that match with (integerp (foo a b c)).

NOTE4    Acl2 Version 1.4 Notes

Once again ld only takes one required argument, as the bind-flg has
been deleted.

Three commands have been added in the spirit of :pe.  :Pe! is similar
to :pe but it prints all events with the given name, rather than just
the most recent.  The command :pf prints the corollary formula
corresponding to a name or rune.  The command :pl (print lemmas) prints
rules whose top function symbol is the given name.  See PE!,
see PF, and see PL.

Book naming conventions have been changed somewhat.  The once-required
.lisp extension is now prohibited!  Directories are supported,
including a notion of "connected book directory".  See
BOOK-NAME.  Also, the second argument of certify-book is now
optional, defaulting to 0.

Compilation is now supported inside the Acl2 loop.  See COMP
and see SET-COMPILE-FNS.

The default color is now part of the Acl2 world; see :doc
default-color.  Ld-color is no longer an ld special.  Instead, colors
are events; see the documentation for red, pink, blue, and gold.

A table exists for controlling whether Acl2 prints comments when it
forces hypotheses of rules; see :doc force-table.  Also, it is now
possible to turn off the forcing of assumptions by disabling the
definition of force; see FORCE.

The event defconstant is no longer supported, but a very similar event,
defconst, has been provided in its place.  See DEFCONST.

The event for defining congruence relations is now defcong (formerly,
defcon).

Patterns are now allowed in :expand hints.  See the documentation for
:expand inside the documentation for hints.

We have improved the way we report rules used by the simplifier.  All
runes of the same type are reported together in the running commentary
associated with each goal, so that for example, executable counterparts
are listed separately from definitions, and rewrite rules are listed
separately from linear rules.  The preprocessor now mentions "simple"
rules; see SIMPLE.

The mechanism for printing warning messages for new rewrite rules,
related to subsumption, now avoids worrying about nonrecursive function
symbols when those symbols are disabled.  These messages have also been
eliminated for the case where the old rule is a :definition rule.

Backquote has been modified so that it can usually provide predictable
results when used on the left side of a rewrite rule.

Time statistics are now printed even when an event fails.

The Acl2 trace package has been modified so that it prints using the
values of the Lisp globals *print-level* and *print-length*
(respectively).

Table has been modified so that the :clear option lets you replace the
entire table with one that satisfies the val and key guards (if any);
see TABLE.

We have relaxed the translation rules for :measure hints to defun, so
that the the same rules apply to these terms that apply to terms in
defthm events.  In particular, in :measure hints mv is treated just
like list, and state receives no special handling.

The loop-stopper test has been relaxed.  The old test required that
every new argument be strictly less than the corresponding old argument
in a certain term-order.  The new test uses a lexicographic order on
term lists instead.  For example, consider the following rewrite rule.

       (equal
        (variable-update var1
                         val1 (variable-update var2 val2 vs))
        (variable-update var2
                         val2 (variable-update var1 val1 vs)))

This rule is permutative.  Now imagine that we want to apply this rule
to the term

       (variable-update u y (variable-update u x vs)).

Since the actual corresponding to both var1 and var2 is u, which is not
strictly less than itself in the term-order, this rule would fail to be
applied in this situation when using the old test.  However, since the
pair (u x) is lexicographically less than the pair (u y) with respect
to our term-order, the rule is in fact applied using our new test.

Messages about events now contain a space after certain left
parentheses, in order to assist emacs users.  For example, the event

       (defthm abc (equal (+ (len x) 0) (len x)))

leads to a summary containing the line

       Form:  ( DEFTHM ABC ...)

and hence, if you search backwards for "(defthm abc", you won't stop at
this message.

More tautology checking is done during a proof; in fact, no goal
printed to the screen, except for the results of applying :use and :by
hints or the top-level goals from an induction proof, are known to Acl2
to be tautologies.

The ld-query-control-alist may now be used to suppress printing of
queries; see LD-QUERY-CONTROL-ALIST.

Warning messages are printed with short summary strings, for example
the string "Use" in the following message.

       Acl2 Warning [Use] in DEFTHM:  It is unusual to :USE an enabled
       :REWRITE or :DEFINITION rule, so you may want to consider
       disabling FOO.

At the end of the event, just before the time is printed, all such
summary strings are printed out.

The keyword command :u has been introduced as an abbreviation for :ubt
:max.  Printing of query messages is suppressed by :u.

The keyword :cheat is no longer supported by any event form.

Some irrelevant formals are detected; see IRRELEVANT-FORMALS.

A bug in the application of metafunctions was fixed: now if the output
of a metafunction is equal to its input, the application of the
metafunction is deemed unsuccessful and the next metafunction is tried.

An example has been added to the documentation for equivalence to
suggest how to make use of equivalence relations in rewriting.

The following Common Lisp functions have been added to Acl2:
alpha-char-p, upper-case-p, lower-case-p, char-upcase, char-downcase,
string-downcase, string-upcase, and digit-charp-p.

A documentation section called proof-checker has been added for the
interactive facility, whose documentation has been slightly improved.
See in particular the documentation for proof-checker, verify, and
macro-command.

A number of events that had been inadvertently disallowed in books are
now permitted in books.  These are:  defcong, defcor, defequiv,
defrefinement, defstub, and verify-termination.

NOTE5    Acl2 Version 1.5 Notes

Acl2 now allows "complex rationals," which are complex numbers whose
real parts are rationals and whose imaginary parts are non-zero
rationals.  See COMPLEX.

A new way of handling forced hypotheses has been implemented.  Rather
than cause a case split at the time the force occurs, we complete the
main proof and then embark on one or more "forcing rounds" in which we
try to prove the forced hypotheses.  See FORCING-ROUND.  To
allow us to compare the new handling of force with the old, Version 1.5
implements both and uses a flag in state to determine which method
should be used.  Do (assign old-style-forcing t) if you want force to
be handled as it was in Version 1.4.  However, we expect to eliminate
the old-style forcing eventually because we think the new style is more
effective.  To see the difference between the two approaches to
forcing, try proving the associativity of append under both settings of
old-style-forcing.  To get the new behavior invoke:

     (thm (implies (and (true-listp a) (true-listp b))
                   (equal (append (append a b) c)
                          (append a (append b c)))))

Then (assign old-style-forcing t) and invoke the thm command above
again.

A new :cases hints allows proof by cases.  See HINTS.

Include-book and encapsulate now restore the acl2-defaults-table when
they complete.  See INCLUDE-BOOK and see ENCAPSULATE.

The guards on many Acl2 primitives defined in axioms.lisp have been
weakened to permit them to be used in accordance with lisp custom and
tradition.

It is possible to attach heuristic filters to :rewrite rules to limit
their applicability.  See SYNTAXP.

A tutorial has been added; see ACL2-TUTORIAL.

Events now print the Summary paragraph listing runes used, time, etc.,
whether they succeed or fail.  The format of the "failure banner" has
been changed but still has multiple asterisks in it.  Thm also prints a
Summary, whether it succeeds or fails; but thm is not an event.

A new event form skip-proofs has been added; see SKIP-PROOFS.

A user-specific customization facility has been added in the form of a
book that is automatically included, if it exists on the current
directory.  See ACL2-CUSTOMIZATION.

A facility for conditional metalemmas has been implemented; see
META.

The acceptable values for ld-skip-proofsp have changed.  In the old
version (Version 1.4), a value of t meant that proofs and local events
are to be skipped.  In Version 1.5, a value of t means proofs (but not
local events) are to be skipped.  A value of 'include-book means proofs
and local events are to be skipped.  There are two other, more obscure,
acceptable values.  See LD-SKIP-PROOFSP.

In order to turn off the forcing of assumptions, one should now disable
the :executable-counterpart of force (rather than the :definition of
force, as in the previous release); see FORCE.

The macros enable-forcing and disable-forcing make it convenient to
enable or disable forcing.  See ENABLE-FORCING and see
DISABLE-FORCING.

The new commands :pr and :pr! print the rules created by an event or
command.  See PR and see PR!.

The new history commands :puff and :puff* will replace a compound
command such as an encapsulate or include-book by the sequence of
events in it.  That is, they "puff up" or "lift" the subevents of a
command to the command level, eliminating the formerly superior command
and lengthening the history.  This is useful if you want to "partially
undo" an encapsulate or book or other compound command so you can
experiment.  See PUFF and see PUFF*.

Theory expressions now are allowed to use the free variable world and
prohibited from using the free variable state.  See THEORIES,
although it is essentially the same as before except it mentions world
instead of state.  See WORLD for a discussion of the Acl2
logical world.  Allowing in-theory events to be state-sensitive
violated an important invariant about how books behaved.

Table keys and values now are allowed to use the free variable world
and prohibited from using the free variable state.  See the note above
about theory expressions for some explanation.

The macro for minus, -, used to expand (- x 3) to (+ x -3) and now
expands it to (+ -3 x) instead.  The old macro, if used in the
left-hand sides of rewrite rules, produced inapplicable rules because
the constant occurs in the second argument of the +, but potential
target terms generally had the constant in the first argument position
because of the effect of commutativity-of-+.

A new class of rule, :linear-alias rules, allows one to implement the
nqthm package and similar hacks in which a disabled function is to be
known equivalent to an arithmetic function.

A new class of rule, :built-in-clause rules, allows one to extend the
set of clauses proved silently by defun during measure and guard
processing.  See BUILT-IN-CLAUSES.

The new command pcb! is like pcb but sketches the command and then
prints its subsidiary events in full.  See PCB!.

:Rewrite class rules may now specify the :loop-stopper field.  See
RULE-CLASSES and see LOOP-STOPPER.

The rules for how loop-stoppers control permutative rewrite rules have
been changed.  One effect of this change is that now when the built-in
commutativity rules for + are used, the terms a and (- a) are permuted
into adjacency.  For example, (+ a b (- a)) is now normalized by the
commutativity rules to (+ a (- a) b); in Version 1.4, b was considered
syntactically smaller than (- a) and so (+ a b (- a)) is considered to
be in normal form.  Now it is possible to arrange for unary functions
be be considered "invisible" when they are used in certain contexts.
By default, unary- is considered invisible when its application appears
in the argument list of binary-+.  See LOOP-STOPPER and see
:DOC set-invisible-fns-table.

Extensive documentation has been provided on the topic of Acl2's "term
ordering."  See TERM-ORDER.

Calls of ld now default ld-error-action to :return rather than to the
current setting.

The command descriptor :x has been introduced and is synonymous with
:max, the most recently executed command.  History commands such as
:pbt print a :x beside the most recent command, simply to indicate that
it *is* the most recent one.

The command descriptor :x-23 is synonymous with (:x -23).  More
generally, every symbol in the keyword package whose first character is
#\x and whose remaining characters parse as a negative integer is
appropriately understood.  This allows :pbt :x-10 where :pbt (:max -10)
or :pbt (:here -10) were previously used.  The old forms are still
legal.

The order of the arguments to defcong has been changed.

The simplifier now reports the use of unspecified built-in type
information about the primitives with the phrase "primitive type
reasoning."  This phrase may sometimes occur in situations where
"propositional calculus" was formerly credited with the proof.

The function pairlis has been replaced in the code by a new function
pairlis$, because Common Lisp does not adequately specify its pairlis
function.

Some new Common Lisp functions have been added, including logtest,
logcount, integer-length, make-list, remove-duplicates, string, and
concatenate.  The source file /slocal/src/acl2/axioms.lisp is the
ultimate reference regarding Common Lisp functions in Acl2.

The functions defuns and theory-invariant have been documented.  See
DEFUNS and see THEORY-INVARIANT.

A few symbols have been added to the list *acl2-exports*.

A new key has been implemented for the acl2-defaults-table,
:irrelevant-formals-ok.  See SET-IRRELEVANT-FORMALS-OK.

The connected book directory, cbd, must be nonempty and begin and end
with a slash.  It is set (and displayed) automatically upon your first
entry to lp.  You may change the setting with set-cbd.  See CBD.

:oops will undo the last :ubt.  See OOPS.

Documentation has been written about the ordinals.  See :DOC e0-ordinalp
and see :DOC e0-ord-<.  [Note added later: Starting with Version_2.8,
instead see O-P and see O<.

The color events -- (red), (pink), (blue), and (gold) -- may no longer
be enclosed inside calls of local, for soundness reasons.  In fact,
neither may any event that sets the acl2-defaults-table.  See
EMBEDDED-EVENT-FORM.

See LD-KEYWORD-ALIASES for an example of how to change the exit
keyword from :q to something else.

The attempt to install a monitor on :rewrite rules stored as simple
abbreviations now causes an error because the application of
abbreviations is not tracked.

A new message is sometimes printed by the theorem prover, indicating
that a given simplification is "specious" because the subgoals it
produces include the input goal.  In Version 1.4 this was detected but
not reported, causing behavior some users found bizarre.  See
SPECIOUS-SIMPLIFICATION.

:Definition rules are no longer always required to specify the :clique
and :controller-alist fields; those fields can be defaulted to
system-determined values in many common instances.  See
DEFINITION.

A warning is printed if a macro form with keyword arguments is given
duplicate keyword values.  Execute (thm t :doc nil :doc "ignored") and
read the warning printed.

A new restriction has been placed on encapsulate.  Non-local recursive
definitions inside the encapsulate may not use, in their tests and
recursive calls, the constrained functions introduced by the
encapsulate.  See SUBVERSIVE-RECURSIONS.  (Note added in
Version  2.3:  Subversive recursions were first recognized by us here
in Version 1.5, but our code for recognizing them was faulty and the
bug was not fixed until Version  2.3.)

The events defequiv, defcong, defrefinement, and defevaluator have been
reimplemented so that they are just macros that expand into appropriate
defthm or encapsulate events; they are no longer primitive events.  See
the documentation of each affected event.

The defcor event, which was a shorthand for a defthm that established a
corollary of a named, previously proved event, has been eliminated
because its implementation relied on a technique we have decided to ban
from our code.  If you want the effect of a defcor in Version 1.5 you
must submit the corresponding defthm with a :by hint naming the
previously proved event.

Error reporting has been improved for inappropriate in-theory hints and
events, and for syntax errors in rule classes, and for non-existent
filename arguments to ld.

Technical Note:  We now maintain the Third Invariant on type-alists, as
described in the Essay on the Invariants on Type-alists, and
Canonicality.  This change will affect some proofs, for example, by
causing a to rewrite more quickly to c when (equiv a b) and (equiv b c)
are both known and c is the canonical representative of the three.

NOTE6    Acl2 Version 1.6 Notes

A new key has been implemented for the acl2-defaults-table, :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 you execute :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 acl2-defaults-table
immediately after execution of an include-book, certify-book, or
encapsulate 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.

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.

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.

The command :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.

A theory ground-zero has been added that contains exactly the enabled
rules in the startup theory.  See GROUND-ZERO.

Define-pc-macro and define-pc-atomic-macro now automatically define
:red functions.  (It used to be necessary, in general, to change color
to :red before invoking these.)

For a proof of the well-foundedness of e0-ord-< on the e0-ordinalps,
see PROOF-OF-WELL-FOUNDEDNESS.  [Note added later: Starting with
Version_2.8, o< and o-p replace e0-ord-< and e0-ordinalp, respectively.]

Free variables are now handled properly for hypotheses of
:type-prescription rules.

When the system is loaded or saved, state is now bound to
*the-live-state*.

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 (:red
or :pink).

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.  Butlast is now
defined.  The definition of integer-length has been modified.  The
left-hand side of the rewrite rule rational-implies2 has been changed
from (* (numerator x) (/ (denominator x))) to (* (/ (denominator x))
(numerator x)), in order to respect the fact that unary-/ is invisible
with respect to binary-*.  See LOOP-STOPPER.

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 and and or terms, in
the goal being simplified.

The function apply is no longer introduced automatically by translation
of user input to internal form when functions are called on
inappropriate explicit values, e.g., (car 3).

The choice of which variable to use as the measured variable in a
recursive definition has been very slightly changed.