DOC

brief documentation (type :doc name) 
Major Section:  DOCUMENTATION

NOTE: The :doc command only makes sense at the terminal. Furthermore it only works at the terminal when a ``full-size'' image has been built. Most users will probably access the ACL2 documentation in other ways, as explained in the file "doc/README" that comes with the ACL2 distribution. 

Examples:
ACL2 !>:doc DEFTHM          ; print documentation of DEFTHM
ACL2 !>:doc logical-name    ; print documentation of LOGICAL-NAME
ACL2 !>:doc "MY-PKG"      ; print documentation of "MY-PKG"


Related Topics:
:more                      ; continues last :doc or :more-doc text
:more-doc name             ; prints more documentation for name
:docs **                   ; lists all documented symbols
:docs "compil"             ; documented symbols apropos "compil"
:DOC documentation         ; describes how documentation works


General Form:
ACL2>:doc logical-name
where logical-name is a logical name (see logical-name) for which you hope there is documentation. Chances are there is no documentation at the moment, but we are working on adding documentation strings for all the user level ACL2 functions.

For a general discussion of our treatment of documentation strings, see documentation.

This is the first cut at online documentation. Users can be particularly helpful by sending mail on the inadequacies of the system. Address it just to Moore and put Documentation in the subject line. There are several things that trouble me about what I've done here.

First, many concepts aren't documented. Ultimately, I'd like to . document (a) every CLTL primitive (e.g., case and coerce) and (b) every ACL2 extension (e.g., aref1 and getprop). But so far I have focussed on documenting (c) the ACL2 system primitives (e.g., defthm and what hints look like). My priorities are (c), then (b), and then (a), following the philosophy that the most unstable features should get online documentation in these early releases. Having gotten the basic documentation in place, I'll document new things as they are added, and in response to your pleas I'll try to add documentation to old things that are widely regarded as important.

Second, I worry that the existing documentation is unhelpful because it provides too much or too little detail, or it provides the detail too far away from where it is needed. Please be on the lookout for this. Did you get what you needed when you appealed to :doc or :more-doc? If not, what was it you needed? Would more cross-references help? Did you get lost in maze of cross-references?