This is documentation for ACL2 Version 3.4
Copyright (C) 2008  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-2-5    ACL2 Version  2.5 (June, 2000) Notes

Important Changes:

Concurrent with the release of ACL2 Version  2.5 is the publication of
two books about ACL2.  See the "Books and Papers about ACL2 and Its
Applications" on the ACL2 Home Page.

The books subdirectory now contains many new certifiable books,
including solutions to the exercises in the two published books and
full scripts for the case studies.  See books/README.html.

Improved Unix Makefile support for book certification has also been
written.  See books/README.html.

The list of symbols in *acl2-exports* has been considerably expanded.
If you have packages built by importing *acl2-exports* you might want
to look carefully at the new value of that constant.  The new value
includes all :logic mode functions as of Version  2.5, as well as all
documented macros and all built-in theorem names.

Include-book and certify-book were modified to have some additional
keyword arguments.  It is possible to certify a book containing
defaxiom and/or skip-proofs events and get warning messages or errors
signaled, according to the settings of these new flags.  In addition,
it is possible to specify in include-book whether the book must be
certified (under penalty of error if not).  The default values of these
new arguments cause warnings to be printed rather than errors signaled.

The above change involved altering the form of certificate files.  When
books certified under previous versions are included, more warnings
will be generated because these books are considered possibly to
contain defaxiom and/or skip-proofs events.

We anticipate further changes to this aspect of books and consider the
current mechanisms (for controlling whether warnings or errors are
signaled) just a prototype.  See also the discussion below of
"soundness related" warnings.  Your suggestions are welcome.

A discrepancy between ACL2 and Common Lisp was fixed, having to do with
declare ignore.  In past versions of ACL2, a formal parameter of a
defun was considered ignored if it was not used in the body, the guard
or the measure of the defun.  That meant that a variable used only in
the guard could not be declared ignored in ACL2; but some Common Lisp
compilers would complain because the variable was not used in the body.
Now, ACL2 considers a variable ignored if it is not used in the body.

ACL2 can now be built in releases 5.0 and later of Allegro Common Lisp.
(Other releases of Allegro Common Lisp and of other lisps continue to
be supported as well.)  This includes Allegro Common Lisp running on
Windows 98 platforms.  John Cowles helped us do some testing and
answered questions for us.  Thanks John!

We incorporated Ruben Gamboa's changes to allow the building of a
variant, ACL2(r), of ACL2, in which the user can reason about the real
numbers using non-standard analysis.  See REAL.  Note that
ACL2(r) and ACL2 have different underlying theories, and books
certified in one system may not be included in the other.  For backward
compatibility and to ensure a smooth transition, ACL2 is built by
default, not ACL2(r).  This is a compile-time switch; see the makefile
for instructions.  There should be no changes to ACL2 resulting from
the capability of building ACL2(r) from the same sources.  Also see
ACKNOWLEDGMENTS for more on the history of ACL2(r).

A large number of bugs (some affecting soundness) were fixed, and many
small new features were added.  See below.

Less Important Changes:

Some warnings are now considered "soundness related," namely, those
that advise you that an uncertified book has been included or that a
book containing DEFAXIOM or SKIP-PROOFS events.  (Technically,
DEFAXIOMs do not imperil soundness in the proof- theoretic sense,
though they may imperil the validity of theorems.  But you sould know
when a book has added an axiom to your logic!)  In previous versions of
ACL2, all warnings were inhibited if the token warning was included in
the argument to set-inhibit-output-lst.  Now, soundness related
warnings are printed even if warnings have been inhibited.  To inhibit
all warnings, supply the token warning! to set-inhibit-output-lst.

Several bugs in defstobj were fixed, relating to the possibility that
some of the subfunctions introduced by the defstobj were already
defined.

:Puff no longer tries to expand defstobj events.  Previously, the
attempt would cause a hard error.

A soundness bug was fixed.  The bug might have been exercised if you
had an alternative definition (implies hyps (equiv (fn ...) body)) in
which equiv is an equivalence relation other than EQUAL.  In this case,
calls of fn might have been expanded to body in places that were not
equiv-hittable.

An obscure soundness bug was fixed.  The bug was exercised only if you
had a metafunction with a computed hypothesis (i.e., a "meta hypothesis
function"), the hypothesis contained a free variable, i.e., a variable
not involved in the term being rewritten, and the free variable
occurred in the output of the metafunction.  The possibility of this
bug was brought to our attention by Robert Krug.

We fixed a bug in the handling of hide related to the question of
whether a variable symbol occurs in a term.  The old code did not find
the variable and could cause the system to throw away a hypothesis
about it on the grounds that it was never mentioned.  Rob Sumners
helped discover this problem.

The handling of :elim rules was generalized, permitting arbitrary known
equivalence relations instead of merely equal in the concluding
equality.

The printing of runes (rule names; see RUNE) used has been made
"deterministic," both in proof output and in proof attempt summaries,
by sorting the runes before printing.

The handling of free variables has been improved for hypotheses such as
(< 0 X), and more generally, any hypotheses involving a comparison with
0 (even for example (< X 1) where X is known to be an integer, which is
handled as (<= X 0)).  Thanks to Robert Krug for bringing relevant
examples to our attention.

A new value, :comp, has been implemented for the :load-compiled-file
keyword of include-book.  If this value is supplied, then a compiled
file will always be loaded, even if that requires creating the compiled
file first.

The event include-book now generates a warning when a compiled file is
expected but not found (see INCLUDE-BOOK).  Formerly, it only
did so when executed at the top level; it failed to generate the
warning when executed on behalf of a surrounding include-book command.

Certain redefinition warnings generated by Allegro Common Lisp have
been eliminated.

A new key has been implemented for the acl2-defaults-table,
:bogus-mutual-recursion-ok, set with :set-bogus-mutual-recursion-ok.
Thanks to David Russinoff for pointing out the utility of such a key.

A bug was fixed in defun-sk that prevented its generated events from
being accepted when guard verification is being performed.  Thanks to
Bill Young for bringing this problem to our attention.  A second bug
was brought to our attention by Pete Manolios, which was causing
certain defun-sk events to be rejected.  That problem has been fixed,
and an "Infected" warning has also been eliminated.

The command good-bye now works with Allegro Common Lisp.

A low-level bug was fixed that could, for example, cause an error such
as "Error: Expected 5 args but received 4 args" when interrupting a
local event.

A bug has been fixed in the proof-checker related to definition
expansion.  Thanks to Pete Manolios for bringing this to our attention
with a simple example.

A bug has been fixed related to the :bdd hint in the presence of
equivalence relations.  Thanks to Pete Manolios for bringing this to our
attention with a simple example.

The functions position and position-equal formerly required the second
argument to be a true list.  In accordance with Common Lisp, we now
also allow the second argument to be a string.  This could cause
earlier proofs about these functions to fail unless true-listp is known
to hold where necessary.

Robert Krug wrote a patch, which has been incorporated, to prevent
certain infinite loops that can arise in linear arithmetic.  Thanks,
Robert!

The macro let* no longer requires the bound variables to be distinct.

An obscure bug was fixed related to congruence rules.  The bug would
sometimes cause ACL2 to behave as though no rules (other than equality)
were available for some argument positions.  Thanks to Pete Manolios for
bringing this bug to our attention.

Documentation topics have been added for hard-error and prog2$, and the
documentation for illegal has been improved.  Thanks to Rob Sumners for
a useful suggestion in the examples in documentation for prog2$ and a
fix in documentation for sublis.

The event form certify-book was made more secure, in that it can now
catch attempts to write a book to disk during its certification.
Thanks to Rob Sumners for pointing out the insecurity of the existing
mechanism.

A Y2K problem was fixed with our applicative handling of dates.

Accessors and updaters for stobjs have been made more efficient when
the underlying lisp is Allegro Common Lisp, by the use of appropriate
simple array declarations.

A raw Lisp break had been possible when a certified book that had no
guard verification was included in a session after
(set-verify-guards-eagerness 2).  This has been fixed.

The keyword command :comp can now be used to compile only raw Lisp
functions, excluding executable counterparts, by supplying the argument
:raw.

Rewrite rule nth-of-character-listp was removed from source file
axioms.lisp since it is essentially subsumed by characterp-nth.

Printing has been sped up.  In one example the improvement was over 50%
in both Allegro and GCL.

We now allow printing in a "downcase" mode, where symbols are printed
in lower case.  All printing functions except print-object$ now print
characters in lower case for a symbol when the ACL2 state global
variable print-case has value :downcase and vertical bars are not
necessary for printing that symbol.  See IO for a discussion of
the macros acl2-print-case and set-acl2-print-case.  The default
printing remains unchanged, i.e., symbols are printed in upper case
when vertical bars are not required.

A low-level printing function (prin1$) was modified so that it is not
sensitive to various Common Lisp globals related to printing.  So for
example, the function fmt is no longer sensitive to the value of Common
Lisp global *print-case*.  (The preceding paragraph explains how to
control the case for printing in ACL2.)

The definition of array1p was fixed so that the :maximum-length of an
array must be strictly greater than the number specified in the
:dimensions field; they may no longer be equal.  This was always the
intention; the documentation (see ARRAYS) has remained
unchanged.  The corresponding change was also made to array2p.  Allegro
Common Lisp formerly caused an error when compress1 was called on an
array where the numbers above were equal; now, we get a guard violation
instead, which is appropriate.

In the context of theories, a name now represents not just the
corresponding :definition rune, as it has done in earlier versions of
ACL2, but also the corresponding :induction rune.  See THEORIES
for a discussion of runic designators.  Most users will rarely, if
ever, notice this change.  One situation where this change will make a
difference is after executing (in-theory (current-theory 'foo))
followed by (in-theory (enable bar)), where function bar is introduced
after event foo, and bar is recursively defined.  The latter in-theory
form now enables the rune (:induction bar), which implies that the
prover can use the induction scheme stored at definition time for bar.
Formerly, the rune (:induction bar) was not enabled by (in-theory
(enable bar)), and hence the induction scheme for bar was ignored even
when explicit :induct hints were supplied.

You may now supply xargs keyword pair :normalize nil in order to
prevent certain definitions from "hanging" when there are many
if-subexpressions.  see DEFUN.

We now translate type declarations of real into guards, as we have
already done for other types such as rational.  For example, (declare
(type real x)) generates the guard (rationalp x).  See
TYPE-SPEC.

The theorem prover now behaves reasonably under the combination of
specifying a value of t both for :otf-flg and for a hint
:do-not-induct.  Previously, it aborted the first time it would have
otherwise pushed a goal for induction, but now, it will continue and
wait until all induction subgoals have been pushed before it aborts.

We changed slightly the definition of round.  However, we believe that
the new definition is equivalent to the old.

The definition of Common Lisp function substitute has been added.

The following changes have been made in the use of file names within
ACL2.  We thank Warren Hunt and John Cowles for running some tests of
these changes on Macintosh and Windows 98 platforms (respectively).

     (1) Names of directories and files now use a syntax like that used
     for Unix (trademark of AT&T), where directories are separated using
     the "/" character even when the operating system is not Unix or
     Linux.  See PATHNAME.  ACL2 also continues to support its
     notion of _structured pathnames_ from Version  2.4 and before, but
     might not do so in future releases and hence no longer documents
     such syntax.

     (2) The command :set-cbd may now take a relative pathname as an
     argument.

     (3) When the macro ld is given a file name as a value for
     standard-oi, then if that file name is a relative pathname it
     refers to the result of prepending the connected book directory
     (see PATHNAME, see CBD, and see SET-CBD)
     in order to obtain an absolute pathname.  Simiarly for the ld
     specials standard-co and proofs-co.

It is no longer necessary to issue :set-state-ok t if you include a
stobj declaration for state, for example:

     (declare (xargs :stobjs state))

See DECLARE-STOBJS.

The proof-checker has been cleaned up a bit, including the
documentation and the capability (once again) to define pc-macro
commands (see DEFINE-PC-MACRO) and proof-checker meta commands
(see DEFINE-PC-META).

Recall that events generate summaries that include a line beginning
with "Warnings:", which is followed (on the same line) by zero or more
brief strings that summarize the warnings generated by that event.
Formerly, this warnings summary for an encapsulate or include-book
event did not include the summary strings for warnings generated by
subsidiary events.  This has been fixed.

Macro cw has been documented and now expands to a call of a ;logic mode
function.  See CW for a way to print to the screen without
having to involve the ACL2 state.  Thanks to Rob Sumners for suggesting
that we document this useful utility.

Functions duplicates, add-to-set-equal, intersection-eq, evens, and
odds are now :logic mode functions.

NOTE-2-5(R)    ACL2 Version  2.5(r) (June, 2000) Notes

Important changes to non-standard version:

Please see NOTE-2-5 for changes to Version  2.5 of ACL2.  We
hope to write more documentation for ACL2(r) in the future.

NOTE-2-6    ACL2 Version  2.6 (November, 2001) Notes

Because of the large number of modifications, we have divided up the
Version  2.6 notes into the following subtopics.

     o New functionality (see NOTE-2-6-NEW-FUNCTIONALITY):
     o Changes in proof engine (see NOTE-2-6-PROOFS):
     o Changes in rules and definitions (see NOTE-2-6-RULES):
     o Guard-related changes (see NOTE-2-6-GUARDS):
     o Proof-checker changes (see NOTE-2-6-PROOF-CHECKER):
     o System-level changes (see NOTE-2-6-SYSTEM):
     o Other (minor) changes (see NOTE-2-6-OTHER):

NOTE-2-6-GUARDS    ACL2 Version  2.6 Notes on Guard-related Changes

When you declare that a function treats certain formals as :stobjs, the
guard of the function is automatically extended to include the
corresponding stobj-recognizer calls.  For example, if a definition
includes (declare (xargs :stobjs (ST))) then the guard of the function
is changed by the addition of the conjunct (ST-P ST).

One impact of this is that if you use the built-in ACL2 state as a
formal parameter of a function, (STATE-P STATE) is added to the guard.
This may introduce a guard where there was none in previous versions of
the system.  In older versions, therefore, no attempt would be made to
verify-guards, while in the new version, we would attempt guard
verification.  You may wish to add (declare (xargs :verify-guards nil))
to such definitions.

A related change affects users who do not use stobjs or state.  In
previous versions of the system -- as now -- a type declaration
extended the guard you provided explicitly.  Thus, if you wrote
(declare (type integer n)) then (INTEGERP n) was added to your guard.
This is still the case and :stobjs recognizers are similarly added.
But in older versions of the system we "added" the conjuncts without
checking whether they were already present in the guard you provided.
This sometimes produced such guards as (and (integerp n) (integerp n))
where the first was produced by your type declaration and the second
was your :guard.  We now eliminate redundant conjuncts; this may
rearrange the order of the conjuncts.

The guard conjectures for functions using stobjs have been simplified
somewhat by taking advantage of the syntactic restrictions checked for
single-threaded objects.

The following functions have been modified so that character and string
arguments are restricted to standard characters.  (See
STANDARD-CHAR-P and see STANDARD-CHAR-LISTP.)

     upper-case-p lower-case-p char-upcase char-downcase
     string-downcase1 string-downcase string-upcase1 string-upcase
     char-equal string-equal1 string-equal

Also, function standard-string-alistp replaces function string-alistp,
with concomitant changes in the guard to assoc-string-equal, and in
variable *acl2-exports*.  Also, lemma
standard-string-alistp-forward-to-alistp replaces lemma
string-alistp-forward-to-alistp.  There is a new lemma
standard-char-p-nth, which has also been added to *acl2-exports*.

The guard had been inadvertently omitted from the definition of the
function substitute (and its subroutine substitute-ac).  This omission
has been corrected; also, the guard is slightly stronger than the
documentation had claimed (and that has been corrected).

NOTE-2-6-NEW-FUNCTIONALITY    ACL2 Version  2.6 Notes on New Functionality

A fundamental change is the provision of the "nu-rewriter" for
simplifying expressions composed of NTH, UPDATE-NTH, and
UPDATE-NTH-ARRAY applications and LET expressions and other calls of
non-recursive functions or LAMBDA expressions involving those symbols.
The nu-rewriter applies the obvious rewrite rule for (NTH i (UPDATE-NTH
j v s)) and the analogous rule for UPDATE-NTH-ARRAY.  See
NU-REWRITER  The nu-rewriter can be enabled with set-nu-rewriter-mode.

A new flag has been added to the xargs of defun permitting the
declaration that the function is non-executable.  The usage is (declare
(xargs :non-executable t)) and the effect is that the function has no
executable counterpart.  On the positive side:  the function is
permitted to use single-threaded object names and functions
arbitrarily, as in theorems rather than as in executable definitions.
Such functions are not permitted to declare any names :stobjs but
accessors, etc., may be used, just as in theorems.

A new flag has been added to permit the system to abbreviate output by
introducing LET* notation identifying common subterms.  The formula
being proved is not affected; this flag changes its displayed form
only.  See set-let*-abstractionp.

A "raw mode" has been added, primarily for faster loading of
applications.  see SET-RAW-MODE.

Functions alphorder and lexorder have been put in :logic mode.
Lexorder is now a total order ordering of the ACL2 universe, and
theorems are included to that effect.  Thanks to Pete Manolios for
suggesting the idea and providing events to use, and to Rob Sumners for
assistance with some modifications.  See also the new book
books/misc/total-order for an irreflexive total order.

The ACL2 user can now make system calls to the host operating system.
See SYS-CALL and see SYS-CALL-STATUS.  Thanks to Rob
Sumners for working out this idea with Pete Manolios and Robert Krug,
who we also thank, and for working out the implementation with us.

It is no longer required to use absolute pathnames in include-book
forms that have been executed before a certify-book.  Any relative
pathname strings in such contexts will be expanded into absolute
pathnames before they are saved in the portcullis of the certificate of
the book being certified.

ACL2 can now be built on top of Allegro Common Lisp 6.0, and also on
Windows platforms on top of Allegro Common Lisp and GCL.  Thanks to Pete
Manolios and Vinay K. Siddhavanahalli for their help with Windows.

Rob Sumners has designed and provided an initial implementation for two
improvements to defstobj (also see STOBJ).  First, array fields
can now be resized.  Resize and length functions are provided for array
fields, which can be used to resize stobj array fields dynamically.
The recognizers for array fields have been simplified to accommodate
this change, so that they only check that each element of the array
field has the specified type.  Second, performance has been improved
for stobjs with a large number of fields, by changing their Common Lisp
implementation to store the fields in a simple vector instead of a list.

Now stobjs may be bound locally; see WITH-LOCAL-STOBJ.  Thanks
to Rob Sumners, who encouraged us to implement this capability, was an
early user of it, and participated usefully in discussions on its
design.

New functions fms!, fmt!, and fmt1! are the same as their respective
functions without the "!," except that the "!" functions are guaranteed
to print forms that can be read back in (at a slight readability cost).

We added extended-metafunctions, metafunctions which allow state and
context sensitive rewriting to some extent.  We thank Robert Krug for
pushing for and on this idea.

The documentation has been improved.  In particular, a new
documentation topic provides a gentle introduction to ACL2 arrays --
see ARRAYS-EXAMPLE -- and additional documentation has been
provided for getting started with proof trees in emacs -- see
PROOF-TREE-EMACS.

New Makefile targets fasl and o have been added to the books/ directory
of the distribution.  For example, you might first certify books using
an ACL2 built on top of GCL (which creates compiled files with suffix
o).  Then, when standing in the books/ directory, you might execute the
command

     make fasl ACL2=my-allegro-acl2

which will create compiled (.fasl) files for Allegro Common Lisp,
assuming that my-allegro-acl2 starts up an ACL2 built on that Common
Lisp.

The macro let* now allows variables to be declared ignored.  See
LET* and see LET.

The user may now control backchaining.  This feature was designed and
primarily implemented by Robert Krug (though the authors of ACL2 are
resposible for any errors); thanks, Robert!  See
BACKCHAIN-LIMIT.

It is now possible to "slow down" the rate at which case splits are
generated by the simplifier.  See SET-CASE-SPLIT-LIMITATIONS.

Accesses to stobjs using nth or update-nth are now displayed using
symbolic constants instead of numeric indices.  For example, given the
event

     (defstobj foo a b :renaming ((b c)))

then the term (nth 0 foo) will be displayed (for example, during
proofs) as (nth *a* foo) while (nth 1 foo) will be displayed as (nth
*c* foo).  The defstobj event now correspondingly introduces a defconst
event for each field accessor function, introducing a constant whose
name is obtained from the accessor's name by prefixing and suffixin a
"*," as in the example above: accessor a generates (defconst *a* 0) and
accessor c generates (defconst *c* 1). See NTH-ALIASES-TABLE
for how to extend this feature for alternate names of stobjs.

Computed hints have been improved.  It is now possible to detect within
a computed hint whether the goal clause is stable under simplification;
it is also possible for a computed hint to change the list of available
hints.  See COMPUTED-HINTS.

It is now possible to provide "default hints" that are appended to the
hints explicitly provided.  See SET-DEFAULT-HINTS.

Using computed hints (see COMPUTED-HINTS) and default hints
(see SET-DEFAULT-HINTS) it is possible to implement a book that
supports "priority phased simplification."  Using this book you can
assign priorities to your rules and cause the theorem prover to
simplify each goal maximally under all the rules of one priority before
enabling rules of the next priority.  See books/misc/priorities.lisp.

The macro defabbrev has been improved to allow declare forms and
documentation strings and to do more error-checking.  Thanks to Rob
Sumners for designing this enhancement and providing the first
implementation.  See DEFABBREV.

Further changes were made to support CMU Lisp.  Wolfhard Buss helped
with these changes.

A new table was added that is used when printing proof output, so that
nests of right-associated calls of a binary function are replaced by
corresponding macro calls, as has been the case for binary-+ and +,
binary-append and append, and so on.  See ADD-BINOP.

Operators logand, logior, logxor, and logeqv are now macros (formerly,
they were functions) that call corresponding binary functions (e.g.,
binary-logand) defined in source file "axioms.lisp".  Thanks to Rob
Sumners for this enhancement.  Proof output will however continue to
show calls of logand, logior, logxor, and logeqv.

Function (allocate-fixnum-range fixnum-lo fixnum-hi) sets aside more
"permanent" fixnums in GCL.

ACL2 now runs under CLISP.  Thanks to Wolfhard Buss and Sam Steingold
for their assistance with the port.

Michael "Bogo" Bogomolny has created a search engine, accessible from
the ACL2 home page.  For that purpose he modified the HTML translator
to create one file per topic (a good idea in any case).  Thanks, Bogo!

An emacs file of potential (but optional) use for ACL2 users may be
found in emacs/emacs-acl2.el.  In particular, this file supports the
use of proof trees (see PROOF-TREE).

Some books have been added or modified.  In particular, Robert Krug has
contributed books/arithmetic-2/, which provides an alternative to the
existing collection of books about arithmetic, books/arithmetic/.  For a
discussion of the distributed books see the link to README.html in the
installation instructions.

NOTE-2-6-OTHER    ACL2 Version  2.6 Notes on Other (Minor) Changes

Warning strings are now case-insensitive.  See
SET-INHIBIT-WARNINGS.

ACL2 causes a warning when an in-theory hint or event causes a 0-ary
function's definition to be disabled but its :executable-counterpart to
be enabled.

A minor modification has been made to defstobj that can have a positive
impact on performance in Allegro Common Lisp.  (For Lisp hackers:  the
stobj name was formerly declared special, and that was disabling
Allegro's tail-merging routing for compilation of some recursive
functions using stobjs.)  The downside is that stobj names can no
longer be evaluated in raw Lisp.  However, raw Lisp is not the right
place to be evaluating ACL2 forms anyhow; see SET-RAW-MODE.  We
thank Rob Sumners for bringing this issue to our attention.

Before Version  2.6, there has been the following problem with defstub
and encapsulate in the case that the current package is not the ACL2
package.  If a signature was specified using the symbol =>, then that
symbol had have been imported into the current package from the ACL2
package when the current package was defined.  There are no longer any
package restrictions on the use of =>.  Thanks to John Cowles for
bringing this problem to our attention.

Bugs in defun-sk have been fixed.  Defun-sk forms introducing functions
of no arguments were failing to be admitted, for example: (defun-sk
always-p1 () (forall (x) (p1 x))).  Thanks to John Cowles for bringing
this problem to our attention.  Also, defun-sk failed on an example in
the documentation (see TUTORIAL4-DEFUN-SK-EXAMPLE), as pointed
out by Matyas Sustik; this bug has been fixed as well.

The trace mechanism has been fixed to handle stobjs, and to avoid the
printing of so-called _enabled structures_.

The brr command :type-alist now produces more readable output.

An include-book of an uncertified book no longer loads an associated
compiled file.

We added a few checks to make sure that the underlying lisp is
suitable, for example checking that the reader is case-insensitive and
reads in symbols with upper-case names where appropriate.

We now warn when forcing (see FORCE) or immediate force mode
(see IMMEDIATE-FORCE-MODEP) change state between enabled and
disabled.  Also see ENABLE-IMMEDIATE-FORCE-MODEP and see
DISABLE-IMMEDIATE-FORCE-MODEP for information about these new macros,
which may be used to control immediate force mode.

We have eliminated the use of a low-level raw Lisp constant,
*most-recent-multiplicity*.  Our test suite saw a speed-up of
approximately 2% as a result for an ACL2 image built on GCL (but no
significant speed-up for an ACL2 image built on Allegro Common Lisp).
We thank Rob Sumners for suggesting this improvement.

Fixnum declarations are now realized as (signed-byte 29) instead of
(signed-byte 27).  We check that the underlying Common Lisp recognizes
objects of type (signed-byte 29) as fixnums, with the exception of
CLISP, which is said to have an efficient bignum implementation.

A new documentation topic functional-instantiation-example illustrates
functional instantiation.

A bug has been fixed in the monitoring of runes (see MONITOR).
Thanks to Dave Greve for sending an example that clearly showed the
problem.

A warning is now issued when it is detected that a :type-prescription
rule may not be as strong as it appears because it is not sufficient to
prove itself by type reasoning.

An error is caused for rules of class :meta when the function symbol IF
is among the :trigger-fns.  (IF was ignored anyhow; the point of this
change is to avoid misleading the user.)

A minor bug has been fixed in :pr, evident for example if this command
was applied to IF.

A minor hole in :set-bogus-mutual-recursion-ok did not permit the
acceptance of mutual-recursion forms that include constant function
definitions.  This has been fixed.  Thanks to Eric Smith for coming up
with a simple example illustrating the problem.

The temporary files "TMP.lisp" and "TMP1.lisp" written out by :comp are
now written to the connected book directory (see CBD).

Previously, the Allegro compiler was not eliminating tail recursion for
executable counterparts of functions, because of the way one of its
flags had been set.  As a result, calls of functions whose guards had
not been verified could run out of stack space when this was not
necessary.  This situation has been fixed.

Executable counterparts could have slow array accesses.  This has been
fixed (specifically, constants are no longer replaced with their values
in the definitions of executable counterparts).

Various improvements have been made to the documentation.  Thanks in
particular to Eric Smith for pointing out a numbers of places where
fixes were in order.

File "mcl-acl2-startup.lisp" has been updated, thanks to feedback from
Philippe Georgelin.

Inefficiencies in GCL fixnum computations were remedied for macros +f
and *f.  Thanks to Rob Sumners for pointing out this issue.

NOTE-2-6-PROOF-CHECKER    ACL2 Version  2.6 Notes on Proof-checker Changes

The proof-checker command =, when used with no arguments, now reports
which hypothesis is being used.

The output from proof-checker command type-alist has been improved.

A slight change has been made to the proof-checker for commands
promote, casesplit, equiv, and =, so that terms of the form (if x nil
y) are recognized as conjunctions, (and (not x) y).  Thanks to Pete
Manolios for suggesting that we consider such a change.

There is a new proof-checker command print-all-concs that prints all
the conclusions of the unproved goals.

A new proof-checker command, runes, has been added.  It reports the
runes that have participated in the interactive proof up to the current
point.

NOTE-2-6-PROOFS    ACL2 Version  2.6 Notes on Changes in Proof Engine

Certain optimizations are performed when converting terms to clausal
form.  For example, (< 0 1) is known to be t, (HARD-ERROR ctx str
alist) is known to be nil, and (INTEGERP n) is known to imply
(RATIONALP n).

In earlier versions of ACL2, the conversion of a term to clausal form
expanded LAMBDA applications.  That may no longer occur.  Some proofs
may slow down (or fail) because your LAMBDA-expressions are not
expanded away when you "expected" them to be.

Robert Krug found a soundness bug in our linear arithmetic package.
The bug was caused by the derivation of an equation from two
inequalities without taking adequate precautions to ensure that both
sides of the inequalities were numeric.  Robert also kindly provided a
fix which we adopted.  Thanks Robert!

We fixed a bug that could prevent the application of a metatheorem.

A bug has been fixed that had caused bogus forcing rounds (see
FORCING-ROUND).  The bug could occur when the hypothesis of a rule
was forced (see FORCE) before the prover decided to start over
and prove the original goal by induction.  Thanks to Rob Sumners for
drawing our attention to this problem.

Some low-level fixes have been made that prevent certain infinite
loops, based on reports by users.  We thank Yunja Choi, Matt Wilding,
and Pete Manolios for reporting such problems.

An obscure potential soundness hole has been fixed by redoing the way
evaluation takes place in the ACL2 loop and during theorem proving.  We
expect that users will see no difference based on this change.  (Those
interested in the details can see the long comment "Essay on Evaluation
in ACL2" in source file interface-raw.lisp.)

A small change was made in computation for a heuristic that controls
backchaining.  This will speed up proofs dramatically in a very few
cases but should have a very small impact in general.

The simplifier has been modified to avoid eliminating hypotheses of
goals that can be established by contextual (specifically, type-set)
reasoning alone.  We believe that this change will generally strengthen
ACL2's reasoning engine, although on rare occasions a lemma that
formerly was provable may require user assistance.  Thanks to Robert
Krug for suggesting this change and providing its implementation.

Case splits are now limited, by default.  This may allow some proof
attempts to provide output where previously the prover would appear to
"go out to lunch."  For a more complete discussion, including
instructions for how users can control case splitting, see
SET-CASE-SPLIT-LIMITATIONS.

A bug has been fixed in the handling of :type-prescription rules by the
bdd package.  Thanks to Rob Sumners for discovering this bug and
supplying a helpful example.

ACL2 may now use the built-in induction scheme for a function symbol
even if that function symbol is disabled.  Formerly, if a function
symbol was disabled then its induction scheme was only considered if an
explicit induction hint was supplied, other than :induct t.

We eliminated the rule-class linear-alias.  This rule class was seldom
used and complicated the linear arithmetic decision procedure in ways
that made it difficult to extend to handle some non-linear special
cases.  The only use of the rule-class that we know of was in our own
nqthm books, which were an attempt to provide an embedding of the Nqthm
logic and theorem prover into ACL2.  But that facility was also
practically never used, as far as we know.  So both linear-alias rules
and the nqthm books have been eliminated.

In earlier versions of ACL2, when the IF-form of (AND p q) was assumed
true - as when rewriting the alpha expression in (IF (AND p q) alpha
beta) - the assumption mechanism did not deduce that p and q are true,
only that their conjunction, in its IF-form, is true.  This has long
been known as a deficiency in both ACL2 and the earlier Nqthm but it
was tedious to do better when one considered the full range of IF-forms
one might encounter in the test of another IF.  Rather than code all
the cases, we just waited until clausification got rid of them.  Robert
Krug developed a pretty nice treatment of the general case and we added
it in this version.  This also involved a surprising number of changes
elsewhere in the system because the improved handling of assumptions
caused the theorem prover often to "erase" hypotheses provided by :use
hints because it could simplify them to t.  Thank you Robert!

In response to a suggestion from Robert Krug, we added mfc-ap so that
extended metafunctions can take advantage of linear arithmetic.  See
EXTENDED-METAFUNCTIONS.

There is less delay in printing goals.  In previous versions, a goal
was not printed until its subgoals were created (or the goal was
proved).  Now, the goal is printed essentially as soon as it is created.

A small technical change has been made in the function term-order, to
give priority on the function symbol count over the weighting of
constants.  So for example, while previously the term (f) preceded the
constant 2, that is no longer the case.  If this change is noticed at
all, it will probably be noticed in how so-called _permutative_ rewrite
rules are applied; see LOOP-STOPPER.  Thanks to Robert Krug for
suggesting this improvement and providing part of the implemtation.

NOTE-2-6-RULES    ACL2 Version  2.6 Notes on Changes in Rules and Constants

The following symbols have been added to the list constant
*common-lisp-specials-and-constants*: REPLACE, FILL, CHARACTER, =,
BREAK, and PRIN1.  This was done in support of ports to Allegro 6.0 and
Windows platforms (see NOTE-2-6-NEW-FUNCTIONALITY).

The list of symbols in *acl2-exports* has been modified, for example to
include show-accumulated-persistence and the legal arguments to
set-inhibit-output-lst.

Functions zp and zip are now handled slightly differently.  They are
are now disabled, but each comes with a :rewrite rule that allows their
expansion on non-variable terms, and also with a :compound-recognizer
rule that avoids the need for opening up these functions when applied
to variables.  The resulting behavior should be very similar to the
behavior of previous versions, except that case splits will be avoided
when these functions are applied to variables.

Function standard-string-alistp replaces function string-alistp.  For
further discussion, see NOTE-2-6-GUARDS.

Rules of class :rewrite whose conclusion is a term of the form (equal
lhs rhs) have always been stored in the expected way:  lhs rewrites to
rhs.  This way of storing :rewrite rules has been extended to allow =,
eq, or eql in place of equal.

Rewrite rule nth-update-nth, in source file axioms.lisp, has been
strengthened.

A new rewrite rule equal-constant-+ has been added to the book
arithmetic/equalities.  This should generally be a beneficial change,
but existing proofs involving the arithmetic books could conceivably be
affected.

Function symbol-package-name and constant *main-lisp-package-name* have
undergone small changes.  This change should rarely be noticed by users
and is discussed elsewhere; see NOTE-2-6-SYSTEM.

We mention here that proofs involving stobjs may need to be modified
because of changes in auxiliary functions generated by defstobj.
(These changes were made in support of a new resizing capability,
mentioned elsewhere in these release notes; see
NOTE-2-6-NEW-FUNCTIONALITY.

In the distributed book directory books/arithmetic/, the book
rationals-with-axioms-proved.lisp has been renamed rationals.lisp.

(ACL2(r) only) Rewrite rules realp-+, realp-*, realp-unary-, and
realp-unary-/ have been added in analogy to existing rules rationalp-+,
rationalp-*, rationalp-unary-, and rationalp-unary-/.  Thanks to Jun
Sawada for suggesting this change.

The definition of aref1 has been modified slightly.  Previously, if
*my-a* were an array then (aref1 'some-name *my-a* :header)  would
evaluate to the cdr of the header of *my-a* rather than to its default.
See ARRAYS.

Changes have been made in the ihs books, based on suggestions from Jun
Sawada, that support its use with ACL2(r) (see REAL).  The
primary change is to replace calls of rationalp with calls of
real/rationalp, which should have no effect on users of standard ACL2.

NOTE-2-6-SYSTEM    ACL2 Version  2.6 Notes on System-level Changes

We modified the tracking of skip-proofs events and the use of state
global ld-skip-proofsp in order to avoid some soundness issues.  For
example, skip-proofs events buried in locally-included books are now
tracked.  The "Essay on Skip-proofs" in source file axioms.lisp gives
several examples of dicey behavior that is no longer supported.

We fixed a problem with some of the makefiles, so that recursive
invocations of make now use the version of make specified on the
command line.

Files were fixed to help non-Unix/Linux users with book certification.
Thanks to John Cowles for finding some problems and suggesting fixes to
books/certify-numbers.lisp, books/arithmetic/certify.lsp, and
books/cowles/certify.lsp.  We thank Scott Burson for noticing and
fixing some other such problems.  Moreover, a bdd test was being
ignored entirely in Version  2.5; this problem has been fixed as well.

A minor change in system function save-acl2-in-allegro will allow this
function to continue to work in Allegro CL versions starting (someday)
with 10.0.  Thanks to Art Flatau for suggesting such a fix.

The books/case-studies/ directory has been removed.  These books are in
support of the first (1998) ACL2 workshop, and are accessible via the
ACL2 home page on the Web at
http://www.cs.utexas.edu/users/moore/acl2/.  Also, the books/cli-misc
directory has been renamed books/misc, and the books/nqthm directory
has been removed.

The notion of ACL2 version has been slightly modified to catch
unsoundness due to implementation dependencies.  See VERSION.
Another change to eliminate such unsoundness is that built-in symbols
now have a symbol-package-name of "COMMON-LISP"; formerly, this string
was "LISP" for ACL2 images built on GCL.  See
SYMBOL-PACKAGE-NAME.  At a low level, the (undocumented) constant
*main-lisp-package-name* is now "COMMON-LISP"; before, it was "LISP"
for GCL.

NOTE-2-6(R)    ACL2 Version  2.6(r) (November, 2001) Notes

Important changes to non-standard version:  None since Version  2.5.

Please see NOTE-2-6 for changes to Version  2.6 of ACL2.  We
hope to write more documentation for ACL2(r) in the future.

NOTE-2-7    ACL2 Version  2.7 (November, 2002) Notes

The Version_2.7 notes are divided into the subtopics below.  Here we
give only a brief summary of a few of the changes that seem most likely
to impact existing proofs.  Not included in this brief summary, but
included in the subtopics, are descriptions of improvements (including
bug fixes and new functionality) that should not get in the way of
existing proof efforts.

In particular, please see NOTE-2-7-NEW-FUNCTIONALITY for
discussion of a number of new features that you may find useful.

Acknowledgements and elaboration, as well as other changes, can be
found in the subtopics listed below.

o Bug fixes (see NOTE-2-7-BUG-FIXES):

     + Three soundness bugs were fixed.  These bugs were probably
     rarely hit, so users may well not notice these changes.

     + Certify-book now requires :skip-proofs-ok t (respectively,
     :defaxioms-okp t) if there are skip-proofs (respectively,
     defaxiom) events in the book or any included sub-books.

     + When :by hints refer to a definition, they now use the original
     body of that definition rather than the simplfied ("normalized")
     body.

     + When ld is applied to a stringp file name, it now temporarily
     sets the connected book directory (see CBD) to the
     directory of that file while evaluating forms in that file.

o New functionality (see NOTE-2-7-NEW-FUNCTIONALITY):

     + ACL2 now works harder to apply :rewrite and :linear rules with
     free variables in the hypotheses.  See
     NOTE-2-7-NEW-FUNCTIONALITY, in particular its first two
     paragraphs, for details.  Forward-chaining also does more with
     free variables.

o Changes in proof engine (see NOTE-2-7-PROOFS):

     + Some prover heuristics have changed slightly.  Among other
     consequences, this can cause subgoal hints to change.  For
     example, suppose that the Version_2.6 proof of a particular
     theorem generated "Subgoal 2" and "Subgoal 1" while Version_2.7
     only generates the second of these.  Then a subgoal hint attached
     to "Subgoal 1" in Version_2.6 would have to be attached to "Goal'"
     in Version_2.7.  (See GOAL-SPEC.)  The full topic has
     details (see NOTE-2-7-PROOFS).

o Changes in rules and definitions (see NOTE-2-7-RULES):

     + The package name of a generated variable has changed for defcong.

o Guard-related changes (see NOTE-2-7-GUARDS):

     + Guard verification formerly succeeded in a few cases where it
     should have failed.

     + Guards generated from type declarations now use functions
     signed-byte-p and unsigned-byte-p, now defined in source file
     axioms.lisp and formerly defined rather similarly under books/ihs/.

o Proof-checker changes (see NOTE-2-7-PROOF-CHECKER):

     + See the above doc topic.

o System-level changes (see NOTE-2-7-SYSTEM):

     + See the above doc topic.

o Other changes (see NOTE-2-7-OTHER):

     + A new table, invisible-fns-table, takes the place of the
     handling of invisible functions in the acl2-defaults-table,

     + The theory-invariant event has been modified so that the default
     action is an error rather than a warning.

     +  Proof output that reports destructor elimination no longer uses
     the word "generalizing".

Again, please proceed to the subtopics for more thorough release notes.