Manual/Guide/guide.tex

21 \def\id{{$\langle${\it id\/}$\rangle$}}
22 \def\th{{$\langle${\it th\/}$\rangle$}}
23 \def\file{{$\langle${\it file}$\rangle$}}
24 \def\filen#1{{$\langle${\it file} #1$\rangle$}}
35 \def\meta#1{\(\langle\){\it #1}\(\rangle\)}
60 conventions used in it.  It also explains how to write entries for the
149 from {\tt Manual/LaTeX/makeindex.bin} if it is present. If not, then an
152 included) and place it in the directory {\tt Manual/LaTeX/makeindex.bin}.
216 scratch, running it through \latex\ twice to ensure consistency of the
251 scratch, running it through \latex\ twice to ensure consistency of the
279 volume and typeset it completely from scratch, running it through \latex\ twice
285 correctly, with all index and page entries resolved, and to rebuild it
291 {\tt Manual} subdirectory {\it of the relevant library directory} and typing
364 {\tt hol/help}, a corresponding file \id\doc\ that documents it. This file is
376 because although it is an ML keyword, it is also an identifier.
479 \filen{1}\sp \filen{2}\sp $\cdots$ \sp \filen{{\it n}}\sp {\tt >}\sp
488 \filen{{\it n}}\doc
496 Note that the shell script {\tt mktex} assumes it is being run in the {\tt
499 resulting {\tt .tex} file in any {\it other\/} directory, one must therefore
505 Because of these pathname dependencies, it is intended that individual authors
522 \item the format used to document pre-proved {\it theorems\/}, and
529 rigid) of the two, so it is explained first.
553 \item the two occurrences of \vsp\ are {\it required\/} single spaces,
576 \noindent The meaning of this theorem is clear only when it is known that
652 \noindent  The theory name `{\it none}' indicates that the theorem is not
657 To make it easy to create documentation for theorems, there are two
680 {Actually for some non-alphanumeric identifiers like {\tt /}, it is necessary
705 \subsubsection{The {\tt {\char'134}DOC} line ({\it required})}
717 \item \vsp\ is a {\it required\/} single space, and
724 \ML\ function, it should {\it not\/} be preceded by the dollar sign
728 every \doc\ file.  There must be exactly one blank line between it and the
737 \subsubsection{The {\tt {\char'134}TYPE} line ({\it required})}
749 \item the three occurrences of \vsp\ are {\it required\/} single spaces,
758 \ML\ function, it must be preceded by the dollar sign `{\small\verb!$!}'.  For
762 blank line between it and the line beginning `{\small\verb!\SYNOPSIS!}'.
801 {\small\verb!thm -> conv!}, but in this case it is clearer to write
825 robust as it could be, but at least it pinpoints mistakes and deliberate typing
845 \subsubsection{The {\tt {\char'134}SYNOPSIS} field ({\it required})}
850 followed by a {\it brief\/} description of the \ML\ identifier being
881 \subsubsection{The {\tt {\char'134}KEYWORDS} field ({\it optional})}
900 \subsubsection{The {\tt {\char'134}LIBRARY} field ({\it optional})}
902 This section is present {\it only} in library documentation, and should be
909 \subsubsection{The {\tt {\char'134}DESCRIBE} field ({\it optional})}
914 almost always a required field; it is omitted only when the item being
926 code, and it should not depend on specific examples in which the function is
931 belong under {\small\verb!\COMMENTS!}.  Failure may be mentioned when it plays
932 a role in the function's behaviour when applied to arguments for which it is
955 \subsubsection{The {\tt {\char'134}FAILURE} field ({\it required})}
968 both failure and looping can occur.  For some functions, it may be difficult to
972 {\small\verb!prove_induction_thm!}.  If the supplied theorem does {\it not\/}
999 \subsubsection{The {\tt {\char'134}EXAMPLE} field ({\it optional})}
1037 \subsubsection{The {\tt {\char'134}USES} field ({\it optional})}
1053 contexts in which it might be used.  For example, suppose that the
1066 \noindent In this case, the {\small\verb!\USES!} field should {\it not\/} be
1097 \subsubsection{The {\tt {\char'134}COMMENTS} field ({\it optional})}
1110 style (e.g.\ `don't use it' in the entry on {\small\verb!POP_ASSUM!}), and so
1118 \subsubsection{The {\tt {\char'134}SEEALSO} field ({\it optional})}
1131 follow the rule: {\em if in doubt, add it}. Note that cross-references must
1148 \subsubsection{The {\tt {\char'134}ENDDOC} line ({\it required})}
1265 to {\tt t[u]}. Although perhaps slightly less intuitive, it is both more formal
1302 consideration, it can be discussed separately.  The addition or subtraction of
1346 \item After the name, give any arguments (e.g.\ terms) that it is applied to in
1388 \bk{DOC}\vsp\meta{name}                            ({\it required} )
1390 \bk{TYPE}\vsp\lb\meta{name}\vsp:\vsp\meta{type}\rb                 ({\it required} )
1392 \bk{SYNOPSIS}                              ({\it required} )
1395 \bk{KEYWORDS}                              ({\it optional})
1397 \bk{LIBRARY}                               ({\it optional})
1399 \bk{DESCRIBE}                              ({\it optional, but usually present} )
1402 \bk{FAILURE}                               ({\it required} )
1405 \bk{EXAMPLE}                               ({\it optional} )
1408 \bk{USES}                                  ({\it optional} )
1411 \bk{COMMENTS}                              ({\it optional} )
1414 \bk{SEEALSO}                               ({\it optional} )
1417 \bk{ENDDOC}                                ({\it required} )
1601 an existing library (such as {\tt `string'} or {\tt `reduce'}) and edit it with
1605 user. As its name suggests, it corresponds to a miniature \DESCRIPTION\