Major Section: DOCUMENTATION
: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-docname that you have read the text provided by
:More-doc just continues spewing out at you the documentation string
provided with a definition. If the user has done his job,
probably remind you of the basics and
:more-doc, if read after
will address obscure details that are nevertheless worth noting.
:more-doc types ``
(type :more for more, :more! for the rest)''
you can get the next block of the continuation by typing
all of the remaining blocks by typing
more!. See more.