src/CTT/README.html
changeset 3279 815ef5848324
parent 1341 69fec018854c
child 15283 f21466450330
--- a/src/CTT/README.html	Wed May 21 17:11:46 1997 +0200
+++ b/src/CTT/README.html	Wed May 21 17:13:00 1997 +0200
@@ -1,23 +1,12 @@
-<HTML><HEAD><TITLE>CTT/ReadMe</TITLE></HEAD><BODY>
+
+<HTML><HEAD><TITLE>CTT/README</TITLE></HEAD><BODY>
 
 <H2>CTT: Constructive Type Theory</H2>
 
-This directory contains the Standard ML sources of the Isabelle system for
-Constructive Type Theory (extensional equality, no universes).  Important
-files include
+This directory contains the ML sources of the Isabelle system for
+Constructive Type Theory (extensional equality, no universes).<p>
 
-<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
-<DD>subdirectory containing examples.  To execute them, enter an ML image
-containing CTT and type: use "ex/ROOT.ML";<P>
-</DL>
+The <tt>ex</tt> subdirectory contains some examples.<p>
 
 Useful references on Constructive Type Theory:
 
@@ -29,4 +18,6 @@
 <LI>	Simon Thompson,<BR>
 	Type Theory and Functional Programming (Addison-Wesley, 1991)
 </UL>
-</BODY></HTML>
+
+</BODY>
+</HTML>