--- a/src/Cube/README.html Wed May 21 17:11:46 1997 +0200
+++ b/src/Cube/README.html Wed May 21 17:13:00 1997 +0200
@@ -1,22 +1,12 @@
-<HTML><HEAD><TITLE>Cube/ReadMe</TITLE></HEAD><BODY>
+
+<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>
+This directory contains the ML sources of the Isabelle system for the
+Lambda-Cube.<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>
+The <tt>ex</tt> subdirectory contains some examples.<p>
NB: the formalization is not completely sound! It does not enforce
distinctness of variable names in contexts!<P>
@@ -28,4 +18,5 @@
Introduction to Generalised Type Systems<BR>
J. Functional Programming
</UL>
-</BODY></HTML>
+</BODY>
+</HTML>