<!-- $Id$ -->
<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>
</DL>
<P>There are several subdirectories. To execute them, issue the command
<PRE>
use_dir "<I><DIR></I>";
</PRE>
where <I><DIR></I> is the desired directory
<DL>
<DT>ex
<DD>general examples
<DT>Auth
<DD>a new approach to verifying authentication protocols
<DT>IMP
<DD>mechanization of a large part of a semantics text by Glynn Winskel
<DT>Integ
<DD>a theory of the integers including efficient integer calculations
<DT>IOA
<DD>extended example of Input/Output Automata (takes a long time to run!)
<DT>Lambda
<DD>a proof of the Church-Rosser theorem for lambda-calculus
<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>