1\chapter*{Preface}\markboth{Preface}{Preface}
2
3This volume is the reference manual for the \HOL\ system.
4It is one of four documents making up the documentation for \HOL:
5
6\begin{myenumerate}
7\item \LOGIC: a formal description of the higher order logic
8  implemented by the \HOL{} system;
9\item \TUTORIAL: a tutorial introduction to \HOL, with case studies;
10\item \DESCRIPTION: a detailed user's guide for the \HOL{} system;
11\item \REFERENCE: the reference manual for \HOL.
12\end{myenumerate}
13
14\noindent These four documents will be referred to by the short names (in
15small slanted capitals) given above.
16
17This document, \REFERENCE, provides documentation on all the pre-defined \ML\
18variable bindings in the \HOL\ system.  These include: general-purpose
19functions, such as \ML\ functions for list processing, arithmetic,
20input/output, and interface configuration; functions for processing the types
21and terms of the \HOL\ logic, for setting up theories, and for using the
22subgoal package; primitive and derived forward inference rules; tactics and
23tacticals; and pre-proved built-in theorems.
24
25% The manual entries for these \ML\ identifiers are divided into two chapters.
26% The first chapter is an alphabetical sequence of manual entries for all \ML\
27% identifiers in the system except those identifiers that are bound to theorems.
28% The theorems are listed in the second chapter, roughly grouped into sections
29% based on subject matter.
30
31The \REFERENCE\ volume is purely for reference and browsing. It is generated
32from the same database that is used by the help system. For an introduction to
33the \HOL\ system, see \TUTORIAL; for a systematic presentation, see
34\DESCRIPTION{}  and \LOGIC{}.
35