% ===================================================================== % HOL Manual LaTeX Source: notes for authors of reference manual % ===================================================================== \documentclass[12pt]{article} \usepackage{fleqn} \usepackage{alltt} \usepackage{,../LaTeX/layout} % --------------------------------------------------------------------- % Read in defined macros and commands % --------------------------------------------------------------------- \input{../LaTeX/commands} \input{../LaTeX/ref-macros} % --------------------------------------------------------------------- % Define a few local macros % --------------------------------------------------------------------- \def\id{{$\langle${\it id\/}$\rangle$}} \def\th{{$\langle${\it th\/}$\rangle$}} \def\file{{$\langle${\it file}$\rangle$}} \def\filen#1{{$\langle${\it file} #1$\rangle$}} \def\doc{{\tt .doc}} \def\jac{{\tt .jac}} \def\bnum#1{{\raise0.6pt\hbox{(}#1\raise0.6pt\hbox{)}}} \def\latex{{\LaTeX}} \def\sp{\hspace*{3.5mm}} \def\vsp{{\tt\char`\ }} \def\bk{{\tt\char`\\ }} \def\lb{{\tt\char`\{}} \def\rb{{\tt\char`\}}} \def\meta#1{\(\langle\){\it #1}\(\rangle\)} \begin{document} \setlength{\unitlength}{1mm} % unit of length = 1mm \setlength{\baselineskip}{16pt} % line spacing = 16pt \pagestyle{plain} % foot = page number % --------------------------------------------------------------------- % Title % --------------------------------------------------------------------- \vskip20mm \begin{center} \LARGE \bf Authors' Guide\\ to writing\\ HOL Documentation \end{center} \vskip20mm \section*{Introduction} This note describes the organization of the \HOL\ documentation and the conventions used in it. It also explains how to write entries for the reference manual and how to write documentation for libraries. All authors of reference manual entries and library documentation should read this document carefully before starting to write. General users of the system may find the beginning sections of this note useful when they wish to typeset the \HOL\ documentation at their site. \section{Structure of the HOL documentation} The \HOL\ system documentation consists of three volumes: \begin{itemize} \item \TUTORIAL, which contains a brief tutorial introduction to the \HOL\ system. This is intended to be the first item read by new users of \HOL\ and provides a self-study introduction to the structure and use of the system. \item \DESCRIPTION, which is intended to serve both as a systematic definition and description of the \HOL\ system, and as an advanced guide for users with some prior experience of the system. \item \REFERENCE, which provides full reference documentation in the form of individual descriptions for all the predefined \ML\ variable bindings in the \HOL\ system. \end{itemize} \noindent In addition, there is a separate volume which is not, strictly speaking, part of the \HOL\ manual set, but which is also described in this note: \begin{itemize} \item \LIBRARIES. This consists of stand-alone documentation for each of the libraries distributed in the \HOL\ system library. \end{itemize} \noindent The documentation in this \LIBRARIES\ volume is written by the contributors of the coresponding \HOL\ system libraries. \section{Structure of the documentation directories} Most of the \LaTeX\ sources for \HOL\ system documentation reside in the subdirectory {\tt Manual} of the main \HOL\ distribution directory. Certain source files for the \REFERENCE\ volume reside in the directory {\tt help}. The reason for this and for the organization of these files is described later in this document. For similar reasons, also explained later, much of the \LIBRARIES\ volume resides in the {\tt Library} directory. The {\tt Manual} directory contains the following subdirectories: \begin{itemize} \item {\tt Description}: \LaTeX\ sources for the \DESCRIPTION\ volume of the documentation. \item {\tt Tutorial}: \LaTeX\ sources for the \TUTORIAL\ volume of the documentation. \item {\tt Reference}: \LaTeX\ sources for the \REFERENCE\ volume of the documentation. \item {\tt Libraries}: {\tt Makefile} for the \LIBRARIES\ volume of the documentation. \item {\tt Covers}: \LaTeX\ and PostScript sources for cover pages for all volumes of the manual. \item {\tt LaTeX}: \LaTeX\ style and macro files for the \HOL\ documentation. \item {\tt Reference/bin}: various sed and shell scripts needed to build the reference manual. \item {\tt Guide}: the \LaTeX\ source for the present document. \end{itemize} \noindent Each of these subdirectories contains a {\tt READ-ME} file explaining its contents. Authors working on parts of the \HOL\ documentation in these directories are advised to first read the appropriate {\tt READ-ME} files. \section{Typesetting the HOL documentation} Each volume of the \HOL\ documentation is typeset using \LaTeX. More specifically, the documentation is designed to be typeset with \LaTeX\ version 2.09 of 7 Dec 1989, based on \TeX, the C version 3.0. Building the documentation also requires the `{\tt makeindex}' program (portable version 2.4). The script {\tt Manual/LaTeX/makeindex} will run the appropriate binary from {\tt Manual/LaTeX/makeindex.bin} if it is present. If not, then an appropriate warning will result: in this case the user should build a binary from the sources in {\tt Manual/LaTeX/makeindex.src} (instructions are included) and place it in the directory {\tt Manual/LaTeX/makeindex.bin}. The \TeX\ psfig macros are required for the fancy cover pages. See Section~\ref{PS} below for further information on this. The following sections describe how to obtain typeset versions of each of the four volumes of the \HOL\ system documentation. \subsection{Choice of paper size} The \HOL\ documentation is designed to be printed either on ISO A4 sized paper (297mm high by 210mm wide) or on American 8.5 by 11 inch paper. The pagination and text size is designed to be identical in both formats. Before typesetting any part of the documentation, the choice of paper size must be set by editing the style file {\tt Manual/LaTeX/layout.sty}. Near the top of this file there is the declaration of a \LaTeX\ boolean flag `{\tt Afour}' followed by a command to set the flag. One may select the paper size by editing this command. For A4 size paper, the appropriate command is `{\tt \bk Afourtrue}' (the distribution default). For American paper, the command should be `{\tt \bk Afourfalse}'. \subsection{Makefile for typesetting the HOL documentation} The {\tt Makefile} in the {\tt Manual} directory allows one to typeset all four volumes of the \HOL\ documentation with a single command. When working in the {\tt Manual} directory, one can type `{\tt make all}' to create typeset versions of the documentation from scratch. Note that the desired paper size should be set before doing this (see above). After \LaTeX\ has typeset the documentation, the following {\tt dvi} files will have been created: \begin{itemize} \item {\tt Tutorial/tutorial.dvi}: the typeset \TUTORIAL\ volume. \item {\tt Description/description.dvi}: the typeset \DESCRIPTION\ volume. \item {\tt Reference/reference.dvi}: the typeset \REFERENCE\ volume. \item {\tt Libraries/libraries.dvi}: a typeset titlepage and preface for the \LIBRARIES\ volume. \end{itemize} \noindent Additionally, the files {\tt Covers/endpages.ps} and {\tt Covers/titlepages.ps} should also be present. These are the PostScript versions of the cover pages for the manual volumes. All these documents are then ready to be printed on a laser-printer. Note that some of them are rather long, and therefore not lightly to be printed. \subsection{Typesetting the tutorial volume} The {\tt Makefile} in the {\tt Tutorial} directory is used to typeset the \TUTORIAL\ volume of the \HOL\ documentation. Working in the {\tt Tutorial} directory, the {\tt make} commands that are implemented are the following: \begin{enumerate} \item Type `{\tt make clean}' to remove all traces of previous executions of \LaTeX\ in this directory. This removes all files with suffixes {\tt .dvi}, {\tt .aux}, {\tt .toc} and {\tt .log}. \item Type `{\tt make tutorial}' to typeset the \TUTORIAL\ volume using \latex. \item Type `{\tt make all}' to typeset the \TUTORIAL\ volume completely from scratch, running it through \latex\ twice to ensure consistency of the references. \end{enumerate} \noindent Note that, as usual, {\tt latex} must be run at least twice to guarantee that various forms of reference (i.e.\ citataions, page references, entries in the table of contents and so on) are consistent. The command `{\tt make tutorial}' (number \bnum{2} above) runs the tutorial volume through \LaTeX\ only once. One may therefore have to type {\tt make tutorial} more than once to guarantee a correct result (twice should be sufficient). Typing `{\tt make all}' is guaranteed to typeset the \TUTORIAL\ volume correctly and completely from scratch. \subsection{Typesetting the description volume} The {\tt Makefile} in the {\tt Description} directory is used to typeset the \DESCRIPTION\ volume of the \HOL\ documentation. Working in the {\tt Description} directory, the {\tt make} commands that are implemented are the following: \begin{enumerate} \item Type `{\tt make clean}' to remove all traces of previous executions of \LaTeX\ in the {\tt Description} directory. This removes all files with suffixes {\tt .dvi}, {\tt .aux}, {\tt .toc}, {\tt .log}, {\tt .idx} and {\tt .ilg}. \item Type `{\tt make description}' to typeset the \DESCRIPTION\ volume using \latex. \item Type `{\tt make index}' to create the \DESCRIPTION\ index. This creates the \LaTeX\ source file {\tt index.tex} using the program {\tt makeindex}. \item Type `{\tt make all}' to typeset the \DESCRIPTION\ volume completely from scratch, running it through \latex\ twice to ensure consistency of the references and the index. \end{enumerate} \noindent As usual, {\tt latex} must be run at least twice to guarantee that various forms of reference are consistent. The command `{\tt make description}' runs the \DESCRIPTION\ through \LaTeX\ only once and does not create the index file. One may therefore have to type {\tt make description} then {\tt make index} and then {\tt make description} again in order to guarantee a correct result (running \DESCRIPTION\ through \LaTeX\ twice should be sufficient). Typing `{\tt make all}' is guaranteed to typeset the \DESCRIPTION\ volume correctly (including index) and completely from scratch. \subsection{Typesetting the reference manual}\label{ref-make-all} The {\tt Makefile} in the {\tt Reference} directory contains entries to typeset the entire \REFERENCE\ manual from scratch, as well as entries for the individual steps required in this process. For a full description of the {\tt make} facilities for \REFERENCE, see section~\ref{ref-make} below; only the {\tt make} facility for building the entire manual is described here. Working in the {\tt Reference} directory, the {\tt make} command for typesetting \REFERENCE\ is: \begin{itemize} \item Type `{\tt make all}' to create the \LaTeX\ sources for the \REFERENCE\ volume and typeset it completely from scratch, running it through \latex\ twice to ensure consistency of the references and the index. \end{itemize} \noindent Typing `{\tt make all}' is guaranteed to typeset \REFERENCE\ correctly, with all index and page entries resolved, and to rebuild it completely from scratch. \subsection{Typesetting the library documentation} Library documentation for a particular library may be typeset by entering the {\tt Manual} subdirectory {\it of the relevant library directory} and typing {\tt make all}. The procedure is essentially the same as that for typesetting one of the main \HOL\ manuals. To make all the library manuals, go into the directory {\tt Manual/Libraries} and type {\tt make all}. This will build manuals for all libraries which have them. Currently, many libraries do not have proper manuals. It is intended that all new libraries should eventually have a proper manual. One or two older libraries (such as {\tt unwind}) have had a manual written for them. More details on {\tt writing} library documentation are given in a later section. Again, the intention is that the format should correspond closely to that for the main documentation. \subsection{Typesetting the cover pages}\label{PS} The {\tt Makefile} in the {\tt Covers} directory is used to typeset the fancy cover pages for all the volumes in the \HOL\ documentation. Working in the {\tt Covers} directory, the {\tt make} variables used are: \begin{enumerate} \item {\small LATEX}: the \LaTeX\ command. \item {\small DVI2PS}: name of the {\small DVI} to PostScript converter. \item {\small DVI2PSOPTS}: options given to {\small DVI2PS}. \end{enumerate} \noindent and the commands that are implemented are the following: \begin{enumerate} \item Type `{\tt make clean}' to remove all traces of previous executions of \LaTeX\ in the {\tt Covers} directory. This removes all files with suffixes {\tt .dvi}, {\tt .aux}, {\tt .toc}, {\tt .log}, {\tt .idx} and {\tt .ilg}. \item Type `{\tt make all}' to typeset the fancy cover pages using \latex and {\small DVI2PS}. \end{enumerate} \noindent {\tt latex} needs to be run only once, and {\small DVI2PS} must be able to understand the \TeX\ psfig macros. We supply a version of the macros, and information on obtaining conversion programs in the directory {\tt Covers/psfig}. \section{Structure of the reference manual} The manual is organized into three chapters. Chapter 1 provides manual entries for all the pre-defined \ML\ identifiers in the \HOL\ system, except the identifiers that are bound to pre-proved theorems. These include: general-purpose functions, such as \ML\ functions list processing, arithmetic, input/output, and interface configuration; functions for processing the types and terms of the \HOL\ logic, for setting up theories, and for using the subgoal package; primitive and derived forward inference rules; and tactics and tacticals. The arrangement of this chapter is strictly alphabetical. Chapter 2 lists all pre-proved theorems built into the system, \mbox{together} with the \ML\ identifiers to which they are bound. These are grouped into sections, based on the `subject matter' of the theorems. The sections describing groups of theorems more or less mirror the \HOL\ theories that contain these theorems. Chapter 3 is the index, which is automatically generated. \section{Structure of the reference manual directory} The reference manual for the system is distributed along with the \HOL\ sources in the directories {\tt hol/Manual/Reference} and {\tt hol/help}. Each predefined \ML\ identifier \id\ should have, somewhere within the directory {\tt hol/help}, a corresponding file \id\doc\ that documents it. This file is used to generate the \latex\ source for the manual entry on the identifier \id. A specification of the format of \id\doc\ files and an explanation of how they are converted into \latex\ sources are given in the sections that follow. Note that a few characters cannot conveniently be used in filenames, so the filename does not follow the \id\doc\ scheme. This will certainly not affect alphanumeric identifiers, and library documenters will not generally have much to worry about. Note that entries do not exist for ML keywords such as {\tt let} and {\tt or}. These are not strictly identifiers. However there is an entry for {\tt do}, because although it is an ML keyword, it is also an identifier. The source files for the manual are in the following subdirectories of the directory {\tt hol/help}: \vspace*{4mm plus2mm minus2mm} \noindent\begin{tabular}{@{\qquad}l@{\hskip4mm ---\hskip4mm}l@{}} {\tt ENTRIES} & all non-theorem identifiers (chapter 1)\\ {\tt THEOREMS} & pre-proved theorems (chapter 2) \end{tabular} \vspace*{4mm plus2mm minus2mm} \noindent The directory {\tt ENTRIES}, simply contains a \doc\ file for each relevant \ML\ identifier in the system. The directory {\tt THEOREMS} contains further subdirectories. These correspond to a classification of built-in theorems by subject matter: \vspace*{4mm plus2mm minus2mm} \noindent\begin{tabular}{@{\qquad}l@{\hskip4mm ---\hskip4mm}l@{}} {\tt arith} & theorems about arithmetic\\ {\tt axioms} & axioms of the \HOL\ logic \\ {\tt basic-logic} & definitions basic logical constants \\ {\tt combin} & theorems about combinators \\ {\tt functions} & basic theorems about functions \\ {\tt list} & theorems about lists \\ {\tt logic} & logical tautologies \\ {\tt one} & theorems about the type \ml{one} \\ {\tt pairs} & theorems about pairs \\ {\tt sum} & theorems about disjoint sums \\ {\tt tree} & theorems about trees \\ {\tt tydefs} & theorems used for type definitions \end{tabular} \vspace*{4mm plus2mm minus2mm} \noindent The manual entries for built-in theorems are in pretty much their final form, and these subdirectories contain a \doc\ file for every built-in theorem. The directory {\tt Reference/bin} contains various shell and {\tt sed} scripts that are used to generate the \LaTeX\ source for \REFERENCE\ from the \doc\ files. These programs are explained in more detail below. \section{Generation of the LaTeX source} Each \id\doc\ file is in a special format (described below), from which the \latex\ source for a manual entry on the \ML\ identifier \id\ can be generated. The file {\tt bin/doc-to-tex.sed} is the {\tt sed} script used to generate \latex\ source text from \doc\ files. Executing: \begin{itemize} \item {\tt sed -f bin/doc-to-tex.sed}\sp \id\doc\sp {\tt >}\sp \file \end{itemize} \noindent will create a file called \file, containing a translation into \latex\ source text of the documentation on the identifier \id\ in the file \id\doc. The shell script {\tt bin/doc-to-tex} finds, sorts and translates all \doc\ files in a given directory into LaTeX sources. This shell script is used to generate chapter 1 of the \REFERENCE\ manual. \subsection{Typesetting the entire manual}\label{ref-make} The {\tt Makefile} in the {\tt Reference} directory can be used to create the \latex\ source for the entire reference manual. The command sequence for doing this, and then typesetting the reference manual, is as follows: \begin{enumerate} \item Type `{\tt make tex}' to create the \latex\ source for the finished manual entries. This translates all \doc\ files into \latex\ and builds a source text for the entire manual from the results. \item Type `{\tt make reference}' to run the file {\tt reference.tex} through \latex\ to typeset the manual. \item Type `{\tt make index}' to create the \latex\ source for the index. \end{enumerate} \noindent Note that steps \bnum{1} and \bnum{2} must be done in that order. Note further that {\tt latex} must be run again after step \bnum{3} to guarantee that the index is consistent with the body of the text. Step \bnum{3} may, of course, be omitted until a final typeset version, complete with index, is required for printing. The \REFERENCE\ makefile also supports the command {\tt make all}, which is described above in section~\ref{ref-make-all}. \subsection{Typesetting individual manual entries} To facilitate the debugging of individual manual entries (\ie\ individual \doc\ files), the shell script {\tt bin/mktex} is provided to generate a stand-alone \latex\ source file from individual \doc\ files. Executing: \begin{itemize} \item {\tt mktex}\sp \filen{1}\sp \filen{2}\sp $\cdots$ \sp \filen{{\it n}}\sp {\tt >}\sp \file{\tt .tex} \end{itemize} \noindent Will translate the \doc\ files: \medskip \noindent \qquad \filen{1}\doc\sp\sp \filen{2}\doc\sp\sp $\cdots$ \sp\sp \filen{{\it n}}\doc \medskip \noindent into a stand-alone \latex\ source file called \file{\tt .tex}, which can then be run through \latex\ in order to inspect the typeset manual entries generated from these files. Note that the shell script {\tt mktex} assumes it is being run in the {\tt Reference} directory, and generates a \latex\ source which makes reference (via relative pathnames) to the directories {\tt ../LaTeX}. To run \latex\ on the resulting {\tt .tex} file in any {\it other\/} directory, one must therefore edit the either the pathnames in this file or the pathnames in the script {\tt mktex} itself. Furthermore, {\tt mktex} makes use of the {\tt sed} script {\tt bin/doc-to-tex.sed} (see above), which therefore must be present in a subdirectory {\tt bin} of the directory in which {\tt mktex} is run. Because of these pathname dependencies, it is intended that individual authors working on the reference manual entries will create their own versions of {\tt mktex} in their own file space. The {\tt mktex} file in {\tt Reference/bin} should not itself be edited. \section{The format of {\tt .doc} files} Documentation for individual \ML\ bindings is written in a very rigid form. This is to enable both \latex\ source for the manual and a plain file for online documentation to be easily generated from a single source. The following sections describe this standard format for \doc\ files and explain the conventions adopted for the form and content of reference manual entries in general. In fact, there are really two distinct formats for \doc\ files: \begin{itemize} \item the format used to document pre-proved {\it theorems\/}, and \item the format used to document other \ML\ bindings (i.e.\ general-purpose \ML\ functions, logic functions, inference rules, tactics, and so on). \end{itemize} \noindent These are explained below in sections~\ref{thsec} and~\ref{othsec} respectively. The format of \doc\ files for theorems is the simpler (and more rigid) of the two, so it is explained first. \subsection{The format of {\tt .doc} files for theorems}\label{thsec} The format of \doc\ files for theorems is simple. For each theorem, there is a corresponding file called \meta{thmname}\doc, where \meta{thmname} is either the \ML\ identifier to which the theorem is bound (or will be bound by autoloading), or the name under which the theorem is stored in a theory file. The format of this \doc\ file is as shown below: \smallskip \begin{holboxed}\begin{alltt} \bk{THEOREM}\vsp\meta{thmname}\vsp\meta{thyname} \(\vdots\) \bk{ENDTHEOREM} \end{alltt}\end{holboxed} \smallskip \noindent where \begin{itemize} \item the two occurrences of \vsp\ are {\it required\/} single spaces, \item \meta{thmname} is the name of the theorem (as discussed above), \item \meta{thyname} is the name of the theory in which the theorem is stored, \item and the lines between {\small\verb!\THEOREM!} and {\small\verb!\ENDTHEOREM!} are the ascii representation of the theorem in question, as printed by the standard \HOL\ theorem pretty-printer. \end{itemize} \noindent No indentation should be added to the text of the theorem as printed by \HOL. The theorem itself should be no more than 75 characters wide on any line (use \ml{set\_margin} if necessary). Theorems should almost always be printed without type annotations (i.e.\ with the \ml{show\_types} flag off). An exception is made for theorems whose content is likely to be obscure unless type information is shown. An example is the built-in theorem: \begin{hol}\begin{verbatim} one_axiom |- !(f:* -> one) (g:* -> one). f = g \end{verbatim}\end{hol} \noindent The meaning of this theorem is clear only when it is known that \ml{f} and \ml{g} are functions that yield values of type \ml{one}. For theorems of this kind, the documentation should contain the result of pretty-printing the theorem with the \ML\ \ml{show\_types} flag turned on. There are certain theorems which are bound to \ML\ identifiers when the system is built, but which are not stored in any theory file. For these theorems, the \doc\ format is: \smallskip \begin{holboxed}\begin{alltt} \bk{THEOREM}\vsp\meta{thmname}\vsp\bk{none} \(\vdots\) \bk{ENDTHEOREM} \end{alltt}\end{holboxed} \smallskip \noindent That is, the string `{\small\verb!\none!}' takes the place of the theory name. This format should also be used in library documentation for theorems which are bound to \ML\ identifiers when a library is loaded, but which are not stored in the library in a theory file (this situation is expected to be rare). \subsubsection{Examples} Shown below is the \doc\ file for the built-in theorem \ml{PRIM\_REC\_THM}: \smallskip \begin{holboxed}\begin{verbatim} \THEOREM PRIM_REC_THM prim_rec |- !x f. (PRIM_REC x f 0 = x) /\ (!m. PRIM_REC x f(SUC m) = f(PRIM_REC x f m)m) \ENDTHEOREM \end{verbatim}\end{holboxed} \smallskip \noindent The \meta{thmname} field in this file is `\ml{PRIM\_REC\_THM}', and the \meta{thyname} field is the theory name `\ml{prim\_rec}'. When typeset in \latex, the reference manual entry generated from this \doc\ file looks like this: {\def\filbreak{\relax} \THEOREM PRIM\_REC\_THM prim\_rec |- !x f. (PRIM_REC x f 0 = x) /\ (!m. PRIM_REC x f(SUC m) = f(PRIM_REC x f m)m) \ENDTHEOREM }\vspace{4mm plus2mm minus1mm} Here is an example showing the \doc\ file for a built-in theorem in which the keyword `{\small\verb!\none!}' is used in the \meta{thyname} field: \smallskip \begin{holboxed}\begin{verbatim} \THEOREM NOT_CLAUSES \none |- (!t. ~~t = t) /\ (~T = F) /\ (~F = T) \ENDTHEOREM \end{verbatim}\end{holboxed} \smallskip \noindent When typeset, this entry looks like: {\def\filbreak{\relax} \THEOREM NOT\_CLAUSES {\none} |- (!t. ~~t = t) /\ (~T = F) /\ (~F = T) \ENDTHEOREM }\vspace{4mm plus2mm minus1mm} \noindent The theory name `{\it none}' indicates that the theorem is not stored in any built-in theory. \subsubsection{Automatically-generated {\tt .doc} files for theorems} To make it easy to create documentation for theorems, there are two functions in the \texttt{Parse} structure to produce directories full of them. The two functions are \begin{itemize} \item \ml{export\_theorems\_as\_docfiles}\sp\meta{directory}\sp \meta{theorem list} \item \ml{export\_theory\_as\_docfiles}\sp\meta{directory} \end{itemize} \noindent The first takes a list of string-theorem pairs and writes them out to \texttt{.doc} files in the given directory. The second does this for all of the axioms, theorems and definitions of the current theory. \subsection{The format of {\tt .doc} files for other identifiers} \label{othsec} In this section, the format and content of \doc\ files for \ML\ identifiers other than those bound to theorems is explained. These identifiers are mostly the names of built-in \ML\ functions. For each identifier \meta{name}, there will (eventually) be a corresponding file called \meta{name}\doc\footnote {Actually for some non-alphanumeric identifiers like {\tt /}, it is necessary to call the file something else.}. The general format of a \doc\ file is shown in Figure~\ref{doc-fig}. The file has several fields, which must appear in the order shown below (though some of the fields are optional). The fields are identified by the keywords: \begin{itemize} \item {\small\verb!\DOC!} \item {\small\verb!\TYPE!} (or {\small\verb!\BLTYPE!} and {\small\verb!\ELTYPE!}) \item {\small\verb!\SYNOPSIS!} \item {\small\verb!\KEYWORDS!} \item {\small\verb!\LIBRARY!} (present only in library documentation) \item {\small\verb!\DESCRIBE!} \item {\small\verb!\FAILURE!} \item {\small\verb!\EXAMPLE!} \item {\small\verb!\USES!} \item {\small\verb!\COMMENTS!} \item {\small\verb!\SEEALSO!} \item {\small\verb!\ENDDOC!} \end{itemize} The format and content of each of these fields is explained in detail in the sections that follow. \subsubsection{The {\tt {\char'134}DOC} line ({\it required})} The first line in each \doc\ file must have the form \medskip \noindent\qquad{\small\verb!\DOC!\vsp\meta{name}} \medskip \noindent where \begin{itemize} \item \vsp\ is a {\it required\/} single space, and \item \meta{name} is the \ML\ identifier being documented. \end{itemize} \noindent If the \ML\ identifier in the \meta{name} field stands for an infix \ML\ function, it should {\it not\/} be preceded by the dollar sign `{\small\verb!$!}'. For example, the \meta{name} field for the tactical {\small\verb!THEN!} should simply be `{\small\verb!THEN!}' and not `{\small\verb!$THEN!}'. The {\small\verb!\DOC!} line is a required field in every \doc\ file. There must be exactly one blank line between it and the {\small\verb!\TYPE!} line. An example {\small\verb!\DOC!} line is shown below: \begin{holboxed}\begin{verbatim} \DOC ACCEPT_TAC \end{verbatim}\end{holboxed} \subsubsection{The {\tt {\char'134}TYPE} line ({\it required})} The third line in each \doc\ file must have the form \medskip \noindent\qquad{\small\verb!\TYPE!\vsp\verb!{!\meta{name}\vsp\ml{:}\vsp\meta{type}\verb!}!} \medskip \noindent where \begin{itemize} \item the three occurrences of \vsp\ are {\it required\/} single spaces, \item \meta{name} is the \ML\ identifier being documented, and \item \meta{type} is the type of the identifier being documented, usually precisely as printed by the system with \ML\ type abbreviations in force (see below). \end{itemize} \noindent If the \ML\ identifier in the \meta{name} field stands for an infix \ML\ function, it must be preceded by the dollar sign `{\small\verb!$!}'. For example, the \meta{name} field for the tactical {\small\verb!THEN!} should be `{\small\verb!$THEN!}', not `{\small\verb!THEN!}'. The {\small\verb!\TYPE!} line is a required field in every \doc\ file. There must be exactly one blank line between it and the line beginning `{\small\verb!\SYNOPSIS!}'. Occasionally the type may be too long to fit on one line. In such circumstances the name and type should be placed on one or more lines, sandwiched between {\small\verb!\BLTYPE!} and {\small\verb!\ELTYPE!} (`begin-long-type' and `end-long-type'), as follows: \medskip \noindent\qquad{\small\verb!\BLTYPE!} \par\noindent\qquad{\small\meta{name}\vsp\ml{:}\vsp\meta{type$_1$}} \par\noindent\qquad{\small\meta{type$_2$}} \par\noindent\qquad\vdots \par\noindent\qquad{\small\meta{type$_n$}} \par\noindent\qquad{\small\verb!\ELTYPE!} \medskip \noindent where \meta{type$_1$}, \ldots, \meta{type$_n$} represent the type broken onto $n$ lines. The type may begin on the second line if that is more appropriate; that is the \meta{name} field and the colon can appear on their own in the first line. When necessary, {\small\verb!\BLTYPE!} and {\small\verb!\ELTYPE!} should be used in place of {\small\verb!\TYPE!}, and all other conventions associated with {\small\verb!\TYPE!} should be adhered to when using them. An example {\small\verb!\TYPE!} line is shown below: \smallskip \begin{holboxed}\begin{verbatim} \TYPE {ACCEPT_TAC : thm_tactic} \end{verbatim}\end{holboxed} \smallskip The type quoted in the {\small\verb!\TYPE!} should almost always be precisely the type shown by the system. An exception is made for types which if abbreviated by the built-in type abbreviations (e.g.\ {\small\verb!conv!}) may be misleading as to the nature of the \ML\ function in question. For example, the type of {\small\verb!AP_THM!} is shown by the system as {\small\verb!thm -> conv!}, but in this case it is clearer to write {\small\verb!(thm -> term -> thm)!} since {\small\verb!AP_THM!} is not really a conversion-generating function. If the {\small\verb!\TYPE!} field differs from the type printed by the system, then the fact should be noted in the {\small\verb!\COMMENTS!} field. Unless there is a very good reason, changing the types quoted by the system should be done in the following circumstances only: \begin{itemize} \item Appearance of {\small\verb!goal!} when a {\small\verb!term list # term!} has no real correspondence with a goal, or anything to do with backwards proof. A good example is {\small\verb!list_mk_forall!}. \item Appearance of {\small\verb!conv!} when a {\small\verb!term -> thm!} is not most naturally thought of as a conversion. {\small\verb!ASSUME!} at least fits uncontroversially into this category. \end{itemize} Most {\small\verb!\TYPE!} fields should agree precisely with the system (even up to bracketing and spacing). The shell script {\small\verb!bin/typecheck!} may therefore be used to check exact correspondence with system types automatically. It is not as robust as it could be, but at least it pinpoints mistakes and deliberate typing changes. The script should be given as an argument the doc-files to be typechecked, for example `{\tt *.doc}'. The following example shows the form of the output, which is from {\tt diff(1)}. {\small \begin{verbatim} /homes/jrh$ cd doc /homes/jrh/doc$ typecheck *.doc 2c2 < ALPHA : (term -> term -> thm) --- > ALPHA : (term -> conv) 5,6c5,6 < AP_THM : (thm -> term -> thm) < ASSUME : (term -> thm) --- > AP_THM : (thm -> conv) > ASSUME : conv \end{verbatim}} \subsubsection{The {\tt {\char'134}SYNOPSIS} field ({\it required})} The {\small\verb!\SYNOPSIS!} field follows the blank line after the previous field, and must be present in every \doc\ file. It consists of a line containing only the keyword `{\small\verb!\SYNOPSIS!}', followed by a {\it brief\/} description of the \ML\ identifier being documented. The text of this description should start on the line immediately following the line beginning `{\small\verb!\SYNOPSIS!}'. There must be exactly one blank line between the text of the synopsis (which is indicated by three dots in Figure~\ref{doc-fig}) and the keyword of the field that follows. The synopsis should consist of at most one or two short sentences (or phrases) which provide a concise but accurate indication of the purpose or function of the \ML\ identifier being documented. The aim of the synopsis is not to give a full specification or description, but merely to allow the reader to decide at a glance whether this item may provide the functionality that he or she is looking for. If at all possible, this should fit on one line on an 80-column display. Unless clearly inappropriate, the synopsis should use the third person singular present tense, for example ``Solves any goal of the form \ldots'', ``Introduces an assumption \ldots'' or ``Performs the action corresponding to \ldots''. Consistency in this regard makes reading a lot of synopsis lines displayed by a help tool less tiresome for the user. An example {\small\verb!\SYNOPSIS!} field for the tactic {\small\verb!ACCEPT_TAC!} is shown below: \smallskip \begin{holboxed}\begin{verbatim} \SYNOPSIS Solves a goal if supplied with the desired theorem (up to alpha-conversion). \end{verbatim}\end{holboxed} \smallskip \subsubsection{The {\tt {\char'134}KEYWORDS} field ({\it optional})} This field is optional. It is intended simply to provide a list of relevant words which can be used by (existing or future) help tools to find an entry when you cannot remember the name, but do know the kind of thing you are looking for. The words should be written on the line(s) below, separated by commas and terminated by a period. Here is an example: \smallskip \begin{holboxed}\begin{verbatim} \KEYWORDS assumptions, rewriting. \end{verbatim}\end{holboxed} \smallskip \subsubsection{The {\tt {\char'134}LIBRARY} field ({\it optional})} This section is present {\it only} in library documentation, and should be followed by a single space and the name of the library. For example: \begin{holboxed}\begin{verbatim} \LIBRARY reduce \end{verbatim}\end{holboxed} \subsubsection{The {\tt {\char'134}DESCRIBE} field ({\it optional})} The {\small\verb!\DESCRIBE!} field consists of a line containing only the keyword `{\small\verb!\DESCRIBE!}', followed by a full description of the \ML\ identifier being documented. The {\small\verb!\DESCRIBE!} field is almost always a required field; it is omitted only when the item being documented is so simple that a complete description is already given by the {\small\verb!\SYNOPSIS!} field. The text of the description should start on the line immediately following the line beginning `{\small\verb!\DESCRIBE!}'. There must be exactly one blank line between the text of the description (which is indicated by three dots in Figure~\ref{doc-fig}) and the keyword of the field that follows. The aim of the {\small\verb!\DESCRIBE!} field is to give a complete and accurate specification of what the \ML\ function\footnote{\dots or other \ML\ data object, but the vast majority of manual entries are for functions.} being documented does. The description should not make reference to the \ML\ source code, and it should not depend on specific examples in which the function is used (these belong under {\small\verb!\EXAMPLES!}). Neither should the description discuss specific situations in which one might use the function in question (this belongs under {\small\verb!\USES!}). Comments of a general nature (e.g.\ `this function really should be reimplemented to do so-and-so') belong under {\small\verb!\COMMENTS!}. Failure may be mentioned when it plays a role in the function's behaviour when applied to arguments for which it is intended (e.g.\ when failure is used for backtracking, as in {\small\verb!REPEAT!} and {\small\verb!ORELSE!}). But a description of failure due to incorrect use of the function (e.g.\ applying {\small\verb!dest_comb!} to a variable) does not belong here; this information should instead be given in the {\small\verb!\FAILURE!} field. As an example, here is the {\small\verb!\DESCRIBE!} field for {\small\verb!ACCEPT_TAC!}: \smallskip \begin{holboxed}\begin{verbatim} \DESCRIBE {ACCEPT_TAC} maps a given theorem {th} to a tactic that solves any goal whose conclusion is alpha-convertible to the conclusion of {th}. \end{verbatim}\end{holboxed} \smallskip \noindent The use of the braces `{\small\verb!{!}' and `{\small\verb!}!}' in this example is explained below in Section~\ref{typesetting}. \subsubsection{The {\tt {\char'134}FAILURE} field ({\it required})} The {\small\verb!\FAILURE!} field consists of a line containing only the keyword `{\small\verb!\FAILURE!}', followed by a full (English language) specification of the conditions under which evaluation can fail when the \ML\ identifier being documented is used. The {\small\verb!\FAILURE!} field is required, even when the function being described cannot fail. The text of the failure specification should start on the line immediately following the line beginning `{\small\verb!\FAILURE!}'. There must be exactly one blank line between the text of this specification (which is indicated by three dots in Figure~\ref{doc-fig}) and the keyword of the field that follows. The {\small\verb!\FAILURE!} field should describe the conditions under which both failure and looping can occur. For some functions, it may be difficult to give both necessary and sufficient conditions for failure. For example, the first argument to the function {\small\verb!INDUCT_THEN!} should be a theorem of the form returned by the built-in function {\small\verb!prove_induction_thm!}. If the supplied theorem does {\it not\/} have this form, {\small\verb!INDUCT_THEN!} will almost certainly fail. It is, however, a feature of the way {\small\verb!INDUCT_THEN!} is implemented that this function may succeed, and even do the intended thing, when supplied with theorems whose form is not precisely that of a theorem proved by {\small\verb!prove_induction_thm!} (users should not depend on this). The {\small\verb!\FAILURE!} field for {\small\verb!INDUCT_THEN!} should make this clear, perhaps by stating that this function succeeds when applied to theorems of the correct form, but `may' fail on other theorems. When the function being documented cannot fail, the formula `Never fails.' should be used. Here is an example {\small\verb!\FAILURE!} field for {\small\verb!ACCEPT_TAC!}: \smallskip \begin{holboxed}\begin{verbatim} \FAILURE {ACCEPT_TAC th (A,g)} fails if the term {g} is not alpha-convertible to the conclusion of the supplied theorem {th}. \end{verbatim}\end{holboxed} \smallskip \noindent The use of the braces `{\small\verb!{!}' and `{\small\verb!}!}' in this example is explained below in Section~\ref{typesetting}. \subsubsection{The {\tt {\char'134}EXAMPLE} field ({\it optional})} The {\small\verb!\EXAMPLE!} field consists of a line containing only the keyword `{\small\verb!\EXAMPLE!}', followed by an illustrative example or examples of the use of the \ML\ identifier being documented. The text of the example should start on the line immediately following the line beginning `{\small\verb!\EXAMPLE!}'. There must be exactly one blank line between the text of this specification (which is indicated by three dots in Figure~\ref{doc-fig}) and the keyword of the field that follows. The {\small\verb!\EXAMPLE!} field is optional, and should be present only when an example will genuinely add to the reader's understanding. In most cases, examples should be accompanied by a running commentary, with the actual \ML\ code displayed (see section~\ref{typesetting}) when necessary. Examples should be constructed such that the reader can run them in a standard virgin \HOL\ session. Examples should avoid using the subgoals package if possible (an exception is documenting the package itself). It is still preferable to give complete \ML\ sessions, but if that is impractical, then give a slightly higher-level description of what is going on. An example is given below: \begin{holboxed}\begin{verbatim} \EXAMPLE The goal: { ?- ?x. x=T } \noindent can be solved by: { EXISTS_TAC "T" THEN REFL_TAC } \end{verbatim}\end{holboxed} \noindent Please remember the {\tt noindent} directive on intermediate non-verbatim lines, if there are any, and that all verbatim displays should be indented by 3 spaces. \subsubsection{The {\tt {\char'134}USES} field ({\it optional})} The {\small\verb!\USES!} field consists of a line containing only the keyword `{\small\verb!\USES!}', followed by a statement of common or typical uses of the \ML\ identifier being documented. The text of the example should start on the line immediately following the line beginning `{\small\verb!\USES!}'. There must be exactly one blank line between the text of this specification (which is indicated by three dots in Figure~\ref{doc-fig}) and the keyword of the field that follows. The {\small\verb!\USES!} field is optional, and is likely to be present only for complex functions such as certain tactics and inference rules. In many cases, the {\small\verb!\SYNOPSIS!} will already have said everything that needs to be said about the uses of a function. A {\small\verb!\USES!} field will not be needed in these cases. The {\small\verb!\USES!} field should not simply state what the function in question does, but should describe general contexts in which it might be used. For example, suppose that the {\small\verb!\SYNOPSIS!} for {\small\verb!SPEC!} is: \smallskip \begin{holboxed}\begin{verbatim} \SYNOPSIS Specializes the leading universally-quantified variable of a theorem to a supplied value. \end{verbatim}\end{holboxed} \smallskip \noindent In this case, the {\small\verb!\USES!} field should {\it not\/} be something like: \smallskip \begin{holboxed}\begin{verbatim} \USES Used for specializing universally-quantified theorems. \end{verbatim}\end{holboxed} \smallskip \noindent since this adds no information at all. If anything, the {\small\verb!\USES!} field for {\small\verb!SPEC!} should be something like: \smallskip \begin{holboxed}\begin{verbatim} \USES Obtaining specific instances of already proved theorems; implementing efficient derived inference rules by appeal to pre-proved general theorems. \end{verbatim}\end{holboxed} \smallskip \noindent But, in the case of {\small\verb!SPEC!}, no {\small\verb!\USES!} field at all is probably more appropriate (in the above, the first `use' is still a paraphrase of the function of {\small\verb!SPEC!}; the second `use' is rather specific, and using {\small\verb!SPEC!} is only a very small part of this kind of activity). \subsubsection{The {\tt {\char'134}COMMENTS} field ({\it optional})} The {\small\verb!\COMMENTS!} field consists of a line containing only the keyword `{\small\verb!\COMMENTS!}', followed by any general remarks about the \ML\ identifier being documented that need to be made but do not belong elsewhere. The text of the example should start on the line immediately following the line beginning `{\small\verb!\COMMENTS!}'. There must be exactly one blank line between the text of this specification (which is indicated by three dots in Figure~\ref{doc-fig}) and the keyword of the field that follows. The {\small\verb!\COMMENTS!} field is optional, and should be used for general remarks about implementation matters, promises of future reimplementation, style (e.g.\ `don't use it' in the entry on {\small\verb!POP_ASSUM!}), and so on. Validity checking should not be mentioned in the comments section. The composition of validity checking steps simply follows the composition of the justification functions created by tactics, so need not be mentioned separately. \subsubsection{The {\tt {\char'134}SEEALSO} field ({\it optional})} The {\small\verb!\SEEALSO!} field consists of a line containing only the keyword `{\small\verb!\SEEALSO!}', followed by list of manual entries relevant to the \ML\ identifier being documented. The list of related entries should start on the line immediately following the line beginning `{\small\verb!\EXAMPLE!}'. The list itself should consist of a sequence of \ML\ identifiers in alphabetical order, separated by commas and (always) terminated by a full stop. There must be exactly one blank line between this list (which is indicated by three dots in Figure~\ref{doc-fig}) and the keyword of the field that follows. When deciding whether to add a cross-reference to the {\verb!SEEALSO!} field, follow the rule: {\em if in doubt, add it}. Note that cross-references must always be ordered alphabetically. Here is a sample {\small\verb!\SEEALSO!} field for {\small\verb!REWRITE_TAC!}: \smallskip \begin{holboxed}\begin{verbatim} \SEEALSO FILTER_ASM_REWRITE_TAC, FILTER_ONCE_ASM_REWRITE_TAC, ONCE_ASM_REWRITE_TAC, ONCE_REWRITE_TAC, PURE_ASM_REWRITE_TAC, PURE_ONCE_ASM_REWRITE_TAC, PURE_ONCE_REWRITE_TAC, PURE_REWRITE_TAC, REWRITE_TAC, SUBST_TAC. \end{verbatim}\end{holboxed} \smallskip \subsubsection{The {\tt {\char'134}ENDDOC} line ({\it required})} The {\small\verb!\ENDDOC!} line, which consists of a single line containing only the keyword `{\small\verb!\ENDDOC!}', signals the end of a manual entry. It must be present in every \doc\ file. \subsection{Using typesetting commands}\label{typesetting} The {\small\verb!\SYNOPSIS!}, {\small\verb!\DESCRIBE!}, {\small\verb!\FAILURE!}, {\small\verb!\EXAMPLE!}, {\small\verb!\USES!}, and {\small\verb!\COMMENTS!} fields of a \doc\ file all consist of a keyword line followed by general text. Within this text, only two kinds of typesetting command are allowed: `{\small\verb%\noindent%}\vsp' at the beginning of a line, and {\small\verb%{%}\meta{text}{\small\verb%}%}. These are interpreted as follows: \begin{enumerate} \item `{\small\verb%\noindent%}\vsp' at the beginning of a line prevents indentation of that line. \item An inline {\small\verb%{%}\meta{text}{\small\verb%}%} results in \meta{text} being typeset in small verbatim font. In particular, `{\small\verb%{%}\meta{text}{\small\verb%}%}' is converted to `{\small\verb!{\small\verb%!}\meta{text}{\small\verb!%}!}'. This means that \meta{text} should not contain the character `{\small\verb!%!}'. \item A sequence of lines of the following form, where `{\small\verb|{|}' and `{\small\verb|}|}' occur at the beginning of otherwise empty lines: \begin{alltt} \verb!{! \vsp\vsp\vsp\(\vdots\) \verb!}! \end{alltt} \noindent gets typeset to displayed verbatim text. \end{enumerate} \noindent When using displayed verbatim text, the lines between `{\small\verb|{|}' and `{\small\verb|}|}' should be manually indented by three spaces. Furthermore, there should be no blank line between the preceding line of text and the open bracket `{\small\verb|{|}' and no blank line between the closing bracket `{\small\verb|}|}' and the following line of text (even if otherwise required by virtue of being the last line in a field). Here is an example of the correct use of the displayed verbatim format: \smallskip \begin{holboxed}\begin{verbatim} from this, we can see that the tactic: { FIRST_ASSUM (\th g. ACCEPT_TAC (SYM th) g ? NO_TAC g) } will search the assumption list for an equation whose symmetric form will solve the current goal. This kind of tactic is very useful when dealing with \end{verbatim}\end{holboxed} \smallskip \noindent Here, there are three spaces manually inserted at the beginning of the displayed line in order to give the finished product the appropriate appearance. The following exception may made to the general rule of indenting displayed text by three spaces: when an example is presented without accompanying commentary, the `displayed' text is not indented. For example, in: \smallskip \begin{holboxed}\begin{verbatim} \EXAMPLE { #length [];; 0 : int #length [1;2;7;1;1];; 5 : int } \end{verbatim}\end{holboxed} \smallskip \noindent no indentation is used, since the `displayed' text is not surrounded by a commentary of ordinary text. \subsection{General conventions}\label{conventions} In addition to the specific conventions laid down in the preceding sections for the text of the various fields in a reference manual entry, the following general conventions should also be observed. \subsubsection{Spelling and terminology.} The `-ize' spelling for words like `generalize', `specialize' is preferred. Use `analyze' rather than `analyse'. The following preferred spellings and hyphenations should also be noted: left-hand side, right-hand side, premise (not premiss), and theorem-tactic. The preferred terms for the parts of theorems, goals, implications and rules are as follows: \begin{itemize} \item An implicative term has an {\em antecedent} and a {\em consequent} \item A theorem or goal has {\em assumptions} and a {\em conclusion} \item A rule has {\em premises} and {\em conclusions} \end{itemize} \noindent It is permissible to use {\em hypotheses} instead of {\em assumptions} if preferred: the two should be regarded as strictly synonymous. The overloading of the word {\em conclusion} is unfortunate, but no viable alternative has been proposed. \subsubsection{Substitution} Substitution of term {\tt u} for a variable {\tt x} in term {\tt t} should be shown as a transition from {\tt t} to {\tt t[u/x]}, rather than from {\tt t[x]} to {\tt t[u]}. Although perhaps slightly less intuitive, it is both more formal and more flexible. Multiple sequential substitutions should be shown as {\tt t[u1/t1]...[un/tn]}, and multiple parallel substitutions as {\tt t[u1,...,un/t1,...,tn]}. The use of {\tt t[u1/t1,...,un/tn]} should be avoided because of the scope for ambiguity. \subsubsection{Goals} Goals with assumptions should be represented by using {\tt ?-} by exact analogy with {\tt |-} for theorems. Thus the goal corresponding to the theorem: \begin{verbatim} x = 0 |- SUC x = 1 \end{verbatim} \noindent would be: \begin{verbatim} x = 0 ?- SUC x = 1 \end{verbatim} \noindent Assumption lists of goals should be shown, even when they do not play a major role. Braces are now free to be used for set-notation without confusion. To get braces into a verbatim section, just double them up: {\tt \{\{A\}\}} etc. \subsubsection{Alpha-equivalence} Alpha-convertibility of terms should not, except in obvious special cases like {\tt ALPHA}, be shown by using different variable names. It is usually sufficient to assume by default that we are dealing with alpha equivalence classes of terms. If important, these issues can be mentioned in the description or comments field. The union (of assumption lists) should be written as an infix lowercase {\tt u}, for example `{\tt A1 u A2}', whether or not alpha-equivalent terms are deemed to be the same when taking the union. If this is an important consideration, it can be discussed separately. The addition or subtraction of an assumption should be written as {\tt A u \{t\}} and {\tt A - \{t\}} respectively, rather than {\tt A} becoming {\tt A,t} or vice versa. \subsubsection{Typesetting inference rules and tactics} The following formats should be followed for rule-style specifications of inference rules and tactics: \medskip \begin{verbatim} -------------- ============ \end{verbatim} \medskip \noindent More precisely, displayed inference rules and tactics in this `rule-notation' should be typeset as follows: \begin{itemize} \item Everything in verbatim mode should be manually indented by 3 spaces. \item Use a line consisting of minus-signs for inference rules, and a line consisting of equal-signs for tactics. \item The line should overlap by exactly one space on either side of the wider of the lines of text above and below. \item The other line of text should be centred within the rule bar as closely as possible. \item Above the line put the theorem(s) or goal prior to application of the rule or tactic (may be empty in the case of theorems). \item Below the line put the theorem(s) or subgoal(s) resulting from application of the rule or theorem. In the case of a tactic which completely solves a goal, this should be a single {\tt -} placed centrally on the bottom line, rather than a completely empty field. \item To the right of the line, after 2 spaces, write the name of the rule or tactic. \item After the name, give any arguments (e.g.\ terms) that it is applied to in order to produce the illustrated effect, except for those which actually appear in the top line of the rule. Sometimes this convention does not make manifest the required order of the arguments; in this case the arguments which appear in the rule line should be restated (see the example of {\small\verb!AP_THM!} given below). When they are written as arguments (only), terms should be put in quotation marks and theorems in parentheses, since this corresponds more closely to an ML expression. \end{itemize} Some examples of rule notation as described above are: \begin{verbatim} A |- x = y ---------------- AP_TERM "f" A |- f x = f y A |- f = g ---------------- AP_THM (A |- f = g) "x" A |- f x = g x A ?- f x = f y ================ AP_TERM_TAC A ?- x = y A ?- ?x. t ============= EXISTS_TAC "u" A ?- t[u/x] \end{verbatim} \newpage \subsection{Format of a {\tt .doc} file} \begin{figure}[h] \begin{holboxed}\begin{alltt} \bk{DOC}\vsp\meta{name} ({\it required} ) \bk{TYPE}\vsp\lb\meta{name}\vsp:\vsp\meta{type}\rb ({\it required} ) \bk{SYNOPSIS} ({\it required} ) \(\vdots\) \bk{KEYWORDS} ({\it optional}) \bk{LIBRARY} ({\it optional}) \bk{DESCRIBE} ({\it optional, but usually present} ) \(\vdots \) \bk{FAILURE} ({\it required} ) \(\vdots \) \bk{EXAMPLE} ({\it optional} ) \(\vdots \) \bk{USES} ({\it optional} ) \(\vdots \) \bk{COMMENTS} ({\it optional} ) \(\vdots \) \bk{SEEALSO} ({\it optional} ) \(\vdots \) \bk{ENDDOC} ({\it required} ) \end{alltt}\end{holboxed} \caption{Format of a \doc\ file.\label{doc-fig}} \end{figure} \newpage \subsection{Example of a {\tt .doc} file} Here is a sample \doc\ file for {\small\verb!ACCEPT_TAC!}: \begin{holboxed}\begin{verbatim} \DOC ACCEPT_TAC \TYPE {ACCEPT_TAC : thm_tactic} \SYNOPSIS Solves a goal if supplied with the desired theorem (up to alpha-conversion). \KEYWORDS tactic. \DESCRIBE {ACCEPT_TAC} maps a given theorem {th} to a tactic that solves any goal whose conclusion is alpha-convertible to the conclusion of {th}. \FAILURE {ACCEPT_TAC th (A,g)} fails if the term {g} is not alpha-convertible to the conclusion of the supplied theorem {th}. \EXAMPLE {ACCEPT_TAC} applied to the axiom { BOOL_CASES_AX = |- !t. (t = T) \/ (t = F) } \noindent will solve the goal { ?- !x. (x = T) \/ (x = F) } \noindent but will fail on the goal { ?- !x. (x = F) \/ (x = T) } \USES Used for completing proofs by supplying an existing theorem, such as an axiom, or a lemma already proved. \SEEALSO MATCH_ACCEPT_TAC. \ENDDOC \end{verbatim}\end{holboxed} \newpage \subsection{Example of a typeset {\tt .doc} file} Here is the typeset documentation for the {\small\verb!ACCEPT_TAC!} \doc\ file shown above: \DOC{ACCEPT\_TAC} \TYPE {\small\verb%ACCEPT_TAC : thm_tactic%}\egroup \SYNOPSIS Solves a goal if supplied with the desired theorem (up to alpha-conversion). \DESCRIBE {\small\verb%ACCEPT_TAC%} maps a given theorem {\small\verb%th%} to a tactic that solves any goal whose conclusion is alpha-convertible to the conclusion of {\small\verb%th%}. \FAILURE {\small\verb%ACCEPT_TAC th (A,g)%} fails if the term {\small\verb%g%} is not alpha-convertible to the conclusion of the supplied theorem {\small\verb%th%}. \EXAMPLE {\small\verb%ACCEPT_TAC%} applied to the axiom {\par\samepage\setseps\small\begin{verbatim} BOOL_CASES_AX = |- !t. (t = T) \/ (t = F) \end{verbatim}} \noindent will solve the goal {\par\samepage\setseps\small\begin{verbatim} ?- !x. (x = T) \/ (x = F) \end{verbatim}} \noindent but will fail on the goal {\par\samepage\setseps\small\begin{verbatim} ?- !x. (x = F) \/ (x = T) \end{verbatim}} \USES Used for completing proofs by supplying an existing theorem, such as an axiom, or a lemma already proved. \SEEALSO MATCH_ACCEPT_TAC. \ENDDOC \newpage \section{Writing library documentation} Libraries should conform to a rigid format, to allow easy interaction with the standard building, typesetting and help tools. The intention is that each library should be organized in the same way as the main \HOL\ directory, with a special {\tt Manual} directory for documentation and a {\tt help} directory for reference entries. \subsection{Directory organization} The standard \HOL\ distribution has a toplevel directory called `Library', which contains one subdirectory for each library, whose name corresponds to the relevant library name. Within this, the following files should exist: \begin{enumerate} \item{\tt Makefile}: this should be a standard Unix Makefile, with at least the following targets. \begin{itemize} \item{\tt all}: this should make object code and theory files (if any) for the entire library \item{\tt clean}: this should remove all object code, but not theory files, if any. \item{\tt clobber}: this should remove object code and theory files. \end{itemize} \item{\tt READ-ME}: this should be a simple text file giving at least: \begin{itemize} \item The name of the library \item A brief description of what the library does (not more than a few lines) \item The author, preferably including an email address \item The date at which the library was written \end{itemize} Other items may be included, but the {\tt READ-ME} file should be kept brief. \item{\tt help} A help directory, containing one or both of the following subdirectories \begin{itemize} \item{\tt ENTRIES}: standard {\tt `.doc'} files for all the \ML\ functions provided by the library, if any \item{\tt THEOREMS}: standard {\tt `.doc'} files for the theorems provided by the library, if any. \end{itemize} These help files should be in the respective standard formats specified above. Note that help files for \ML\ functions should have a {\tt `LIBRARY'} field giving the name of the relevant library. \item{\tt Manual}: a subdirectory for the library documentation. This is described in more detail in the next section. \item Other files, such as \ML\ source, compiled object code, theory files, and any other files the library may need for some reason. Everything connected with documentation should go in the Manual directory. \end{enumerate} \subsection{The Manual directory} The {\tt `Manual'} directory should contain the following files. \begin{enumerate} \item{\tt Makefile}: this should be a standard Unix Makefile to build a dvi version of the library documentation. It should include at least the following targets. \begin{itemize} \item{\tt all}: make the dvi for the entire library documentation \item{\tt clean}: remove dvi files and unnecessary intermediate or auxiliary files produced by a run of \latex. \end{itemize} The reference section for \ML\ functions and theorems will be created automatically from the help directory. Examining a Makefile from an existing library (such as {\tt `string'} or {\tt `reduce'}) will show the general format to make this procedure work. \item{\tt title.tex}: this is a standard file containing a title page for library documentation. The simplest way to make such a file is to copy one from an existing library (such as {\tt `string'} or {\tt `reduce'}) and edit it with the new library name and author's name and address. \item{\tt description.tex}: this is the main documentation file written by the user. As its name suggests, it corresponds to a miniature \DESCRIPTION\ document for the library, explaining in reasonable detail its purpose and usage, probably mentioning some of the \ML\ functions and/or theorems provided, but not embarking on an exhaustive list. \item{\tt entries-intro.tex}: a brief paragraph to act as an introduction to the reference section of \ML\ functions. Apart from the library name, this can again be copied from an existing library. \item{\tt theorems-intro.tex}: a brief paragraph to act as an introduction to the reference section of theorems. Apart from the library name, this can again be copied from an existing library. \item{\tt references.tex}: a standard \latex\ list of any references made in the description section. \end{enumerate} \end{document}