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