% =====================================================================
% 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}
     <premises>                         <goal>
   --------------  <name & args>     ============  <name & args>
    <conclusion>                      <subgoals>
\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}
