a continuation of the :doc documentation

NOTE: The :more-doc command only makes sense at the terminal.

ACL2 !>:more-doc DEFTHM
ACL2 !>:more-doc logical-name
Often 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 ``(type :more for more, :more! for the rest)'' you can get the next block of the continuation by typing :more or all of the remaining blocks by typing :more!. See more.