src/Cube/README
changeset 2077 477e80fe0e9b
parent 2076 ec8857a115af
child 2078 b198b3d46fb4
--- a/src/Cube/README	Wed Oct 09 13:38:11 1996 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-		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
-