author clasohm
Tue, 24 Oct 1995 14:45:35 +0100
changeset 1294 1358dc040edb
parent 0 a5a9c433f639
permissions -rw-r--r--
added calls of init_html and make_chart; added usage of qed

		Cube: Barendregt's Lambda-Cube

This directory contains the Standard ML sources of the Isabelle system for
the Lambda-Cube.  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.ML -- examples file.  To execute them, enter an ML image
containing Cube and type:    use "ex.ML";

NB: the formalization is not completely sound!  It does not enforce
distinctness of variable names in contexts!

For more information about the Lambda-Cube, see
	H. Barendregt
	Introduction to Generalised Type Systems
	J. Functional Programming