:
doc
documentation
Major Section: DOCUMENTATION
NOTE: The :more-doc
command only makes sense at the terminal.
Examples: ACL2 !>:more-doc DEFTHM ACL2 !>:more-doc logical-nameOften it is assumed in the text provided by
:more-doc
name that
you have read the text provided by :doc name
.
:More-doc
just continues spewing out at you the documentation string
provided with a definition. If the user has done his job, :
doc
will
probably remind you of the basics and :more-doc
, if read after :
doc
,
will address obscure details that are nevertheless worth noting.
When :more-doc
types ``(cont'd)
'' you can get the next block of the
continuation by typing :
more
or all of the remaining blocks by
typing :
more!
. See more.