author clasohm
Fri, 17 Nov 1995 12:40:09 +0100
changeset 1339 f1a3a7b44ff1
parent 923 ff1574a81019
permissions -rw-r--r--
converted README to HTLM; replaced "CHOL" by "HOL"

	   HOL: Higher-Order Logic with curried functions

This directory contains the Standard ML sources of the Isabelle system for
Higher-Order Logic with curried functions.  Important files include

ROOT.ML -- loads all source files.  Enter an ML image containing Pure
Isabelle and type:    use "ROOT.ML";

Makefile -- compiles the files under Poly/ML or SML of New Jersey

ex -- subdirectory containing examples.  To execute them, enter an ML image
containing HOL and type:    use "ex/ROOT.ML";

Subst -- subdirectory defining a theory of substitution and unification.

Useful references on Higher-Order Logic:

	P. B. Andrews,
	An Introduction to Mathematical Logic and Type Theory
	(Academic Press, 1986).

	J. Lambek and P. J. Scott,
	Introduction to Higher Order Categorical Logic (CUP, 1986)