Manual/Guide/guide.tex

105 source files for the \REFERENCE\ volume reside in the directory {\tt help}. The
134 \item {\tt Guide}: the \LaTeX\ source for the present document.
248 the \LaTeX\ source file {\tt index.tex} using the program {\tt makeindex}.
365 used to generate the \latex\ source for the manual entry on the identifier \id.
378 The source files for the manual are in the following subdirectories of the
423 that are used to generate the \LaTeX\ source for \REFERENCE\ from the \doc\
426 \section{Generation of the LaTeX source}
429 \latex\ source for a manual entry on the \ML\ identifier \id\ can be generated.
431 source text from \doc\ files. Executing:
438 \latex\ source text of the documentation on the identifier \id\ in the file
446 \latex\ source for the entire reference manual.  The command sequence for
451 \item Type `{\tt make tex}' to create the \latex\ source for the finished
453 source text for the entire manual from the results.
458 \item Type `{\tt make index}' to create the \latex\ source for the index.
475 \latex\ source file from individual \doc\ files.  Executing:
492 \noindent into a stand-alone \latex\ source file called \file{\tt .tex}, which
497 Reference} directory, and generates a \latex\ source which makes reference (via
513 This is to enable both \latex\ source for the manual and a plain file for
514 online documentation to be easily generated from a single source. The following
925 documented does.  The description should not make reference to the \ML\ source
1572 \item Other files, such as \ML\ source, compiled object code, theory files, and