<HTML><HEAD><TITLE>HOL/ReadMe</TITLE></HEAD><BODY>
<H2>HOL: Higher-Order Logic with curried functions</H2>
This directory contains the Standard ML sources of the Isabelle system for
Higher-Order Logic with curried functions. Important files include
<DL>
<DT>ROOT.ML
<DD>loads all source files. Enter an ML image containing Pure
Isabelle and type: use "ROOT.ML";<P>
<DT>Makefile
<DD>compiles the files under Poly/ML or SML of New Jersey<P>
<DT>ex
<DD>subdirectory containing examples. To execute them, enter an ML image
containing HOL and type: use "ex/ROOT.ML";<P>
<DT>Subst
<DD>subdirectory defining a theory of substitution and unification.
</DL>
Useful references on Higher-Order Logic:
<UL>
<LI>P. B. Andrews,<BR>
An Introduction to Mathematical Logic and Type Theory<BR>
(Academic Press, 1986).
<LI>J. Lambek and P. J. Scott,<BR>
Introduction to Higher Order Categorical Logic (CUP, 1986)
</UL>
</BODY></HTML>