Manual/Guide/guide.tex

2 % HOL Manual LaTeX Source: notes for authors of reference manual
61 reference manual and how to write documentation for libraries.  All authors of
62 reference manual entries and library documentation should read this document
88 speaking, part of the \HOL\ manual set, but which is also described in this
127 for all volumes of the manual.
132 reference manual.
197 versions of the cover pages for the manual volumes.  All these documents are
266 \subsection{Typesetting the reference manual}\label{ref-make-all}
269 the entire \REFERENCE\ manual from scratch, as well as entries for the
272 {\tt make} facility for building the entire manual is described here.  Working
298 all new libraries should eventually have a proper manual. One or two older
299 libraries (such as {\tt unwind}) have had a manual written for them.
340 \section{Structure of the reference manual}
342 The manual is organized into three chapters.  Chapter 1 provides manual entries
359 \section{Structure of the reference manual directory}
361 The reference manual for the system is distributed along with the \HOL\ sources
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
418 \noindent The manual entries for built-in theorems are in pretty much their
429 \latex\ source for a manual entry on the \ML\ identifier \id\ can be generated.
441 to generate chapter 1 of the \REFERENCE\ manual.
443 \subsection{Typesetting the entire manual}\label{ref-make}
446 \latex\ source for the entire reference manual.  The command sequence for
447 doing this, and then typesetting the reference manual, is as follows:
452 manual entries.  This translates all \doc\ files into \latex\ and builds a
453 source text for the entire manual from the results.
456 \latex\ to typeset the manual.
471 \subsection{Typesetting individual manual entries}
473 To facilitate the debugging of individual manual entries (\ie\ individual \doc\
493 can then be run through \latex\ in order to inspect the typeset manual entries
506 working on the reference manual entries will create their own versions of {\tt
513 This is to enable both \latex\ source for the manual and a plain file for
516 conventions adopted for the form and content of reference manual entries in
619 typeset in \latex, the reference manual entry generated from this \doc\ file
924 data object, but the vast majority of manual entries are for functions.} being
1121 keyword `{\small\verb!\SEEALSO!}', followed by list of manual entries
1151 only the keyword `{\small\verb!\ENDDOC!}', signals the end of a manual entry.
1237 the text of the various fields in a reference manual entry, the following