src/LCF/README
author clasohm
Fri, 03 Mar 1995 12:04:45 +0100
changeset 925 15539deb6863
parent 0 a5a9c433f639
permissions -rw-r--r--
new version of HOL/Integ with curried function application

		LCF: Logic for Computable Functions

This directory contains the Standard ML sources of the Isabelle system for
LCF.  It is loaded upon FOL, not Pure Isabelle.  Important files include

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

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

ex.ML -- files containing examples.  To execute them, enter an ML image
containing LCF and type:    use "ex.ML";

Useful references on LCF:

	Lawrence C. Paulson,
	Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)