		Search-engine friendly clone of the ACL2 documentation.

Proof-builder-commands

ACL2-pc::doc

(macro) access documentation inside the interactive proof-builder

Examples:

(doc rewrite)          -- documentation on rewriting in ACL2
(doc acl2-pc::rewrite) -- documentation on the proof-builder rewrite command
(doc)                  -- same as (help doc) or (doc acl2-pc::doc)
doc                    -- same as above

General Forms:
(doc) ; or, just: help
(doc topic-name)

For any documentation topic, A, (doc A) prints documentation on A to the terminal. You can read that documentation online or in the Emacs ACL2-Doc browser; see documentation. This proof-builder command provides a direct interface to the ACL2 :doc command at the terminal.

Also see ACL2-pc::help, which provides help for proof-builder commands. For example, submitting (help rewrite) to the proof-builder is equivalent to submitting (doc acl2-pc::rewrite) to the proof-builder, which corresponds to submitting :doc acl2-pc::rewrite directly to the ACL2 loop.