Manual/Guide/guide.tex

363 predefined \ML\ identifier \id\ should have, somewhere within the directory
365 used to generate the \latex\ source for the manual entry on the identifier \id.
376 because although it is an ML keyword, it is also an identifier.
393 relevant \ML\ identifier in the system.  The directory {\tt THEOREMS} contains
429 \latex\ source for a manual entry on the \ML\ identifier \id\ can be generated.
438 \latex\ source text of the documentation on the identifier \id\ in the file
535 the \ML\ identifier to which the theorem is bound (or will be bound by
678 the names of built-in \ML\ functions.  For each identifier \meta{name}, there
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
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
850 followed by a {\it brief\/} description of the \ML\ identifier being
859 the \ML\ identifier being documented.  The aim of the synopsis is not to give
913 \ML\ identifier being documented. The {\small\verb!\DESCRIBE!} field is
960 identifier being documented is used.  The {\small\verb!\FAILURE!} field is
1003 examples of the use of the \ML\ identifier being documented.  The text of the
1041 the \ML\ identifier being documented.  The text of the example should start on
1101 \ML\ identifier being documented that need to be made but do not belong
1122 relevant to the \ML\ identifier being documented.  The list of related entries