--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/README.html	Fri Nov 17 13:22:50 1995 +0100
@@ -0,0 +1,31 @@
+<HTML><HEAD><TITLE>Cube/ReadMe</TITLE></HEAD><BODY>
+
+<H2>Cube: Barendregt's Lambda-Cube</H2>
+
+This directory contains the Standard ML sources of the Isabelle system for
+the Lambda-Cube.  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>
+
+<DT>ex
+examples file. To execute them, enter an ML image
+containing Cube and type: use "ex.ML";
+</DL>
+
+NB: the formalization is not completely sound!  It does not enforce
+distinctness of variable names in contexts!<P>
+
+For more information about the Lambda-Cube, see
+
+<UL>
+<LI>H. Barendregt<BR>
+    Introduction to Generalised Type Systems<BR>
+    J. Functional Programming
+</UL>
+</BODY></HTML>