1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
<html>
<head><title>MORE-DOC.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>MORE-DOC</h2>a continuation of the <code>:</code><code><a href="DOC.html">doc</a></code> <a href="DOCUMENTATION.html">documentation</a>
<pre>Major Section: <a href="DOCUMENTATION.html">DOCUMENTATION</a>
</pre><p>
NOTE: The <code>:more-doc</code> command only makes sense at the terminal.
<pre>
Examples:
ACL2 !>:more-doc DEFTHM
ACL2 !>:more-doc logical-name
</pre>
Often it is assumed in the text provided by <code>:more-doc</code> name that
you have read the text provided by <code>:doc name</code>.
<p>
<code>:More-doc</code> just continues spewing out at you the <a href="DOCUMENTATION.html">documentation</a> string
provided with a definition. If the user has done his job, <code>:</code><code><a href="DOC.html">doc</a></code> will
probably remind you of the basics and <code>:more-doc</code>, if read after <code>:</code><code><a href="DOC.html">doc</a></code>,
will address obscure details that are nevertheless worth noting.<p>
When <code>:more-doc</code> types ``<code>(type :more for more, :more! for the rest)</code>''
you can get the next block of the continuation by typing <code>:</code><code><a href="MORE.html">more</a></code> or
all of the remaining blocks by typing <code>:</code><code><a href="MORE_bang_.html">more!</a></code>. See <a href="MORE.html">more</a>.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
