Manual/Guide/guide.tex

178 versions of the documentation from scratch.  Note that the desired paper size
199 that some of them are rather long, and therefore not lightly to be printed.
205 directory, the {\tt make} commands that are implemented are the following:
221 \noindent Note that, as usual, {\tt latex} must be run at least twice to
222 guarantee that various forms of reference (i.e.\ citataions, page references,
234 Description} directory, the {\tt make} commands that are implemented are the
256 \noindent As usual, {\tt latex} must be run at least twice to guarantee that
292 {\tt make all}. The procedure is essentially the same as that for typesetting
297 them. Currently, many libraries do not have proper manuals. It is intended that
302 section. Again, the intention is that the format should correspond closely to
303 that for the main documentation.
321 \noindent and the commands that are implemented are the following:
344 identifiers that are bound to pre-proved theorems. These include:
354 describing groups of theorems more or less mirror the \HOL\ theories that
364 {\tt hol/help}, a corresponding file \id\doc\ that documents it. This file is
367 are converted into \latex\ sources are given in the sections that follow.
369 Note that a few characters cannot conveniently be used in filenames, so
374 Note that entries do not exist for ML keywords such as {\tt let} and {\tt or}.
423 that are used to generate the \LaTeX\ source for \REFERENCE\ from the \doc\
462 \noindent Note that steps \bnum{1} and \bnum{2} must be done in that order.
463 Note further that {\tt latex} must be run again after step \bnum{3} to
464 guarantee that the index is consistent with the body of the text. Step \bnum{3}
496 Note that the shell script {\tt mktex} assumes it is being run in the {\tt
505 Because of these pathname dependencies, it is intended that individual authors
576 \noindent The meaning of this theorem is clear only when it is known that
577 \ml{f} and \ml{g} are functions that yield values of type \ml{one}.  For
652 \noindent  The theory name `{\it none}' indicates that the theorem is not
703 sections that follow.
780 $n$ lines. The type may begin on the second line if that is more appropriate;
781 that is the \meta{name} field and the colon can appear on their own in the
854 three dots in Figure~\ref{doc-fig}) and the keyword of the field that
861 at a glance whether this item may provide the functionality that he or she is
915 documented is so simple that a complete description is already given by the
920 Figure~\ref{doc-fig}) and the keyword of the field that follows.
946 {ACCEPT_TAC} maps a given theorem {th} to a tactic that solves any goal whose
965 Figure~\ref{doc-fig}) and the keyword of the field that follows.
974 however, a feature of the way {\small\verb!INDUCT_THEN!} is implemented that
976 theorems whose form is not precisely that of a theorem proved by
979 clear, perhaps by stating that this function succeeds when applied to theorems
1007 Figure~\ref{doc-fig}) and the keyword of the field that follows.
1013 be constructed such that the reader can run them in a standard virgin \HOL\
1018 sessions, but if that is impractical, then give a slightly higher-level
1034 non-verbatim lines, if there are any, and that all verbatim displays should be
1045 the field that follows.
1049 cases, the {\small\verb!\SYNOPSIS!} will already have said everything that
1053 contexts in which it might be used.  For example, suppose that the
1101 \ML\ identifier being documented that need to be made but do not belong
1106 that follows.
1128 keyword of the field that follows.
1131 follow the rule: {\em if in doubt, add it}. Note that cross-references must
1166 indentation of that line.
1171 `{\small\verb!{\small\verb%!}\meta{text}{\small\verb!%}!}'. This means that
1198 from this, we can see that the tactic:
1295 sufficient to assume by default that we are dealing with alpha equivalence
1346 \item After the name, give any arguments (e.g.\ terms) that it is applied to in
1440 {ACCEPT_TAC} maps a given theorem {th} to a tactic that solves any goal whose
1484 {\small\verb%ACCEPT_TAC%} maps a given theorem {\small\verb%th%} to a tactic that solves any goal whose
1517 standard building, typesetting and help tools. The intention is that each
1566 Note that help files for \ML\ functions should have a {\tt `LIBRARY'} field