searching the documentation

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 ( has a link to this manual, which as of this writing may be found directly by visiting the following web page: You can build a local copy of this manual from the ACL2 Community Books, following instructions in their Makefile.