\chapter*{Preface}\markboth{Preface}{Preface}

This volume is the reference manual for the \HOL\ system.
It is one of four documents making up the documentation for \HOL:

\begin{myenumerate}
\item \LOGIC: a formal description of the higher order logic
  implemented by the \HOL{} system;
\item \TUTORIAL: a tutorial introduction to \HOL, with case studies;
\item \DESCRIPTION: a detailed user's guide for the \HOL{} system;
\item \REFERENCE: the reference manual for \HOL.
\end{myenumerate}

\noindent These four documents will be referred to by the short names (in
small slanted capitals) given above.

This document, \REFERENCE, provides documentation on all the pre-defined \ML\
variable bindings in the \HOL\ system.  These include: general-purpose
functions, such as \ML\ functions for 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; tactics and
tacticals; and pre-proved built-in theorems.

% The manual entries for these \ML\ identifiers are divided into two chapters.
% The first chapter is an alphabetical sequence of manual entries for all \ML\
% identifiers in the system except those identifiers that are bound to theorems.
% The theorems are listed in the second chapter, roughly grouped into sections
% based on subject matter.

The \REFERENCE\ volume is purely for reference and browsing. It is generated
from the same database that is used by the help system. For an introduction to
the \HOL\ system, see \TUTORIAL; for a systematic presentation, see
\DESCRIPTION{}  and \LOGIC{}.