Manual/Guide/guide.tex

35 \def\meta#1{\(\langle\){\it #1}\(\rangle\)}
534 a corresponding file called \meta{thmname}\doc, where \meta{thmname} is either
542 \bk{THEOREM}\vsp\meta{thmname}\vsp\meta{thyname}
555 \item \meta{thmname} is the name of the theorem (as discussed above),
557 \item \meta{thyname} is the name of the theory in which the theorem is stored,
588 \bk{THEOREM}\vsp\meta{thmname}\vsp\bk{none}
617 \noindent The \meta{thmname} field in this file is  `\ml{PRIM\_REC\_THM}',
618 and the \meta{thyname} field is the theory name `\ml{prim\_rec}'. When
632 keyword `{\small\verb!\none!}' is used in the \meta{thyname} field:
662 \item \ml{export\_theorems\_as\_docfiles}\sp\meta{directory}\sp
663   \meta{theorem list}
665 \item \ml{export\_theory\_as\_docfiles}\sp\meta{directory}
678 the names of built-in \ML\ functions.  For each identifier \meta{name}, there
679 will (eventually) be a corresponding file called \meta{name}\doc\footnote
710 \noindent\qquad{\small\verb!\DOC!\vsp\meta{name}}
719 \item \meta{name} is the \ML\ identifier being documented.
723 \noindent If the \ML\ identifier in the \meta{name} field stands for an infix
725 `{\small\verb!$!}'.  For example, the \meta{name} field for the tactical
742 \noindent\qquad{\small\verb!\TYPE!\vsp\verb!{!\meta{name}\vsp\ml{:}\vsp\meta{type}\verb!}!}
750 \item \meta{name} is the \ML\ identifier being documented, and
751 \item \meta{type} is the type of the identifier being documented, usually
757 \noindent If the \ML\ identifier in the \meta{name} field stands for an infix
759 example, the \meta{name} field for the tactical {\small\verb!THEN!} should be
771 \par\noindent\qquad{\small\meta{name}\vsp\ml{:}\vsp\meta{type$_1$}}
772 \par\noindent\qquad{\small\meta{type$_2$}}
774 \par\noindent\qquad{\small\meta{type$_n$}}
779 where \meta{type$_1$}, \ldots, \meta{type$_n$} represent the type broken onto
781 that is the \meta{name} field and the colon can appear on their own in the
1161 and {\small\verb%{%}\meta{text}{\small\verb%}%}. These are interpreted as
1168 \item  An inline {\small\verb%{%}\meta{text}{\small\verb%}%} results in
1169 \meta{text} being typeset in small verbatim font.  In particular,
1170 `{\small\verb%{%}\meta{text}{\small\verb%}%}' is converted to
1171 `{\small\verb!{\small\verb%!}\meta{text}{\small\verb!%}!}'. This means that
1172 \meta{text} should not contain the character `{\small\verb!%!}'.
1388 \bk{DOC}\vsp\meta{name}                            ({\it required} )
1390 \bk{TYPE}\vsp\lb\meta{name}\vsp:\vsp\meta{type}\rb                 ({\it required} )