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 `args`

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