How To Find Out about ACL2 Functions (cont)
The ACL2 documentation is also available in Emacs, via the ACL2-Doc
browser (see ACL2-Doc)
In addition, runtime images of ACL2 have the hyperlinked text as a large ACL2 data structure that can be explored with ACL2's :doc command. If you have ACL2 running, try the command :doc endp.
Another way to find out about ACL2 functions, if you have an ACL2 image
available, is to use the command
Of course, the ACL2 documentation can also be printed out as a very long book but we do not recommend that! See the ACL2 Home Page to download the Postscript.
Now let's continue with