Manual/Guide/guide.tex

23 \def\file{{$\langle${\it file}$\rangle$}}
24 \def\filen#1{{$\langle${\it file} #1$\rangle$}}
138 \noindent Each of these subdirectories contains a {\tt READ-ME} file explaining
166 be set by editing the style file {\tt Manual/LaTeX/layout.sty}.  Near the top
167 of this file there is the declaration of a \LaTeX\ boolean flag `{\tt Afour}'
248 the \LaTeX\ source file {\tt index.tex} using the program {\tt makeindex}.
259 create the index file.  One may therefore have to type {\tt make description}
364 {\tt hol/help}, a corresponding file \id\doc\ that documents it. This file is
392 \noindent The directory {\tt ENTRIES}, simply contains a \doc\ file for each
419 final form, and these subdirectories contain a \doc\ file for every built-in
428 Each \id\doc\ file is in a special format (described below), from which the
430 The file {\tt bin/doc-to-tex.sed} is the {\tt sed} script used to generate \latex\
434 \item {\tt sed -f bin/doc-to-tex.sed}\sp  \id\doc\sp {\tt >}\sp \file
437 \noindent will create a file called \file, containing a translation into
438 \latex\ source text of the documentation on the identifier \id\ in the file
455 \item Type `{\tt make reference}' to run the file {\tt reference.tex} through
475 \latex\ source file from individual \doc\ files.  Executing:
480 \file{\tt .tex}
492 \noindent into a stand-alone \latex\ source file called \file{\tt .tex}, which
499 resulting {\tt .tex} file in any {\it other\/} directory, one must therefore
500 edit the either the pathnames in this file or the pathnames in the script {\tt
507 mktex} in their own file space.  The {\tt mktex} file in {\tt Reference/bin}
513 This is to enable both \latex\ source for the manual and a plain file for
534 a corresponding file called \meta{thmname}\doc, where \meta{thmname} is either
536 autoloading), or the name under which the theorem is stored in a theory file.
537 The format of this \doc\ file is as shown below:
582 system is built, but which are not stored in any theory file.  For these
598 which are not stored in the library in a theory file (this situation is
603 Shown below is the \doc\ file for the built-in theorem \ml{PRIM\_REC\_THM}:
617 \noindent The \meta{thmname} field in this file is  `\ml{PRIM\_REC\_THM}',
619 typeset in \latex, the reference manual entry generated from this \doc\ file
631 Here is an example showing the \doc\ file for a built-in theorem in which  the
679 will (eventually) be a corresponding file called \meta{name}\doc\footnote
681 to call the file something else.}.
683 The general format of a \doc\ file is shown in Figure~\ref{doc-fig}.  The file
707 The first line in each \doc\ file must have the form
728 every \doc\ file.  There must be exactly one blank line between it and the
739 The third line in each \doc\ file must have the form
761 line is  a required field in every \doc\ file.  There must be exactly one
848 previous field, and must be present in every \doc\ file.  It
1152 It must be present in every \doc\ file.
1158 {\small\verb!\COMMENTS!} fields of a \doc\ file all consist of a keyword line
1384 \subsection{Format of a {\tt .doc} file}
1419 \caption{Format of a \doc\ file.\label{doc-fig}}
1424 \subsection{Example of a {\tt .doc} file}
1426 Here is a sample \doc\ file for {\small\verb!ACCEPT_TAC!}:
1471 \subsection{Example of a typeset {\tt .doc} file}
1473 Here is the typeset documentation for the {\small\verb!ACCEPT_TAC!} \doc\ file
1545 \item{\tt READ-ME}: this should be a simple text file giving at least:
1554 Other items may be included, but the {\tt READ-ME} file should be kept brief.
1599 \item{\tt title.tex}: this is a standard file containing a title page for
1600 library documentation. The simplest way to make such a file is to copy one from
1604 \item{\tt description.tex}: this is the main documentation file written by the