Manual/Guide/guide.tex

570 type information is shown.  An example is the built-in theorem:
631 Here is an example showing the \doc\ file for a built-in theorem in which  the
725 `{\small\verb!$!}'.  For example, the \meta{name} field for the tactical
731 An example {\small\verb!\DOC!} line is shown below:
759 example, the \meta{name} field for the tactical {\small\verb!THEN!} should be
786 An example {\small\verb!\TYPE!} line is shown below:
799 be misleading as to the nature of the \ML\ function in question.  For example,
814         proof. A good example is {\small\verb!list_mk_forall!}.
827 typechecked, for example `{\tt *.doc}'. The following example shows the form of
864 person singular present tense, for example ``Solves any goal of the form
869 An example {\small\verb!\SYNOPSIS!} field for the tactic
889 Here is an example:
903 followed by a single space and the name of the library. For example:
939 As an example, here is the {\small\verb!\DESCRIBE!} field for
953 this example is explained below in Section~\ref{typesetting}.
969 give both necessary and sufficient conditions for failure.  For example, the
983 Here is an example {\small\verb!\FAILURE!} field for
997 this example is explained below in Section~\ref{typesetting}.
1002 keyword `{\small\verb!\EXAMPLE!}', followed by an illustrative example or
1004 example should start on the line immediately following the line beginning
1010 an example will genuinely add to the reader's understanding.  In most cases,
1019 description of what is going on. An example is given below:
1041 the \ML\ identifier being documented.  The text of the example should start on
1053 contexts in which it might be used.  For example, suppose that the
1102 elsewhere.  The text of the example should start on the line immediately
1193 example of the correct use of the displayed verbatim format:
1213 text by three spaces: when an example is presented without accompanying
1214 commentary, the `displayed' text is not indented.  For example, in:
1300 u}, for example `{\tt A1 u A2}', whether or not alpha-equivalent terms are
1350 the rule line should be restated (see the example of {\small\verb!AP_THM!}