Major Section: MISCELLANEOUS
The :doc and :doc! commands will display, at the
terminal, documentation topics defined in ACL2 or in books that
have already been included. The :docs command allows you to search
the documentation at the terminal. See docs.
But how can you find documentation for books that are not included in the current ACL2 session?
The xdoc manual is a combined manual for the ACL2 sources and the community
books. It is built using documentation not only from the ACL2 sources
(which is rearranged) but also from the community books (whether included in
the current session or not), using an ``xdoc processor'' created by Jared
Davis. The ACL2 home page
(http://www.cs.utexas.edu/users/moore/acl2/) has a link to this manual,
which as of this writing may be found directly by visiting the following web
page: http://fv.centtech.com/acl2/latest/doc/. You can build a local
copy of this manual from the ACL2 Community Books, following instructions in
their Makefile.
