Manual/Guide/guide.tex

60 conventions used in it.  It also explains how to write entries for the
203 The {\tt Makefile} in the {\tt Tutorial} directory is used to typeset the
232 The {\tt Makefile} in the {\tt Description} directory is used to typeset the
307 The {\tt Makefile} in the {\tt Covers} directory is used to typeset the
309 the {\tt Covers} directory, the {\tt make} variables used are:
365 used to generate the \latex\ source for the manual entry on the identifier \id.
369 Note that a few characters cannot conveniently be used in filenames, so
412    {\tt tydefs}         & theorems used for type definitions
423 that are used to generate the \LaTeX\ source for \REFERENCE\ from the \doc\
430 The file {\tt bin/doc-to-tex.sed} is the {\tt sed} script used to generate \latex\
440 \doc\ files in a given directory into LaTeX sources. This shell script is used
445 The {\tt Makefile} in the {\tt Reference} directory can be used to create the
522 \item the format used to document pre-proved {\it theorems\/}, and
523 \item the format used to document other \ML\ bindings (i.e.\ general-purpose
596 theory name. This format should also be used in library documentation for
632 keyword `{\small\verb!\none!}' is used in the \meta{thyname} field:
783 should be used in place of {\small\verb!\TYPE!}, and all other conventions
823 {\small\verb!bin/typecheck!} may therefore be used
884 words which can be used by (existing or future) help tools to find an entry
927 used (these belong under {\small\verb!\EXAMPLES!}). Neither should the
933 intended (e.g.\ when failure is used for backtracking, as in
960 identifier being documented is used.  The {\small\verb!\FAILURE!} field is
981 documented cannot fail, the formula `Never fails.' should be used.
1053 contexts in which it might be used.  For example, suppose that the
1108 The {\small\verb!\COMMENTS!} field is optional, and should be used for general
1231 \noindent no indentation is used, since the `displayed' text is not surrounded
1287 a major role. Braces are now free to be used for set-notation without