ACL2 Version 2.0

Here are the two common entries to the documentation graph:
Major Topics (Table of Contents)  
Index of all documented topics 
Here is how we recommend you use this documentation.
If you are a newcomer to ACL2, we do not recommend that you wander off into the full documentation. Instead start with the tours the tours.
If you are a serious ACL2 student and have taken the tours and done the tutorials, we recommend you read selected topics from ``Major Topics'':
DEFUN
and DEFTHM
Finally, experienced users tend mostly to use the ``Index'' to lookup concepts mentioned in error messages or vaguely remembered from their past experiences with ACL2.
Note: If ACL2 has been installed on your local system, the HTML documentation
should also be available locally. You can minimize network traffic by
browsing your local copy. Suppose ACL2 was installed on
/usr/jones/acl2/v20
. Then the local URL for this page is
file:/usr/jones/acl2/v20/acl2sources/doc/HTML/acl2doc.html
.
Many ACL2 users set a browser bookmark to this file and use their browser to
access the documentation during everyday use of ACL2. If you obtain ACL2,
please encourage users to use the local copy of the documentation rather than
access it across the Web.
Note: The documentation is available in four forms: 3.5 megabytes of postscript
(which prints as an 800 page book), HTML, EMAC's Texinfo, and ACL2's own :DOC
commands. The
documentation, in all four forms, is distributed with the source code for the
system. See the doc/
subdirectory of the directory upon which ACL2
is installed.
In its native state, ACL2 ``knows'' very little about arithmetic and other
commonly used mathematical theories. Such knowledge is imparted to ACL2 in the
form of ``books'' written by users; books contain definitions and theorems that
ACL2 interprets as rules to guide its search for a proof. Users have
written some books that may help you. We list a few of them here. The pathnames
below are relative to the books/
subdirectory of the ACL2 directory.
arithmetic/topwithmeta
 elementary arithmetic
datastructures/listdefuns
 definitions of list functions
datastructures/listdefthms
 theorems about list functions
datastructures/deflist
 a tool for defining typed lists
datastructures/listtheory
 brings in all three of the above books
datastructures/setdefuns
 definitions of set functions
datastructures/setdefthms
 theorems about set functions
datastructures/settheory
 brings in both the definitions and theorems
datastructures/alistdefuns
 definitions of alist functions
datastructures/alistdefthms
 theorems about alist functions
datastructures/defalist
 a tool for defining typed alists
datastructures/alisttheory
 brings in all three of the above books
datastructures/numberlistdefuns
 definitions about lists of numbers
datastructures/numberlistdefthms
 theorems about number list functions
datastructures/numberlisttheory
 brings in both the definitions and theorems
datastructures/structures
 a tool for definining typed record structures
(includebook name)
, where name
is the full pathname of the
book.
An infix syntax for ACL2 has been implemented by Michael Smith. Two capabilities are supported.
Function idiv (m : integer, n : integer  n ~= 0) { ifix ( m/n ) }; /* Idiv takes two integer arguments, the second of which cannot = zero */ Theorem distributivityofminusoverplus {(x + y) = x + y}; Theorem carnth0 { consp(x) > x.car = x[0] };