diff -r 636322bfd057 -r 815ef5848324 src/CTT/README.html
--- 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 @@
-CTT/ReadMe
+
+CTT/README
CTT: Constructive Type Theory
-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).
-
-- 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
-
- subdirectory containing examples. To execute them, enter an ML image
-containing CTT and type: use "ex/ROOT.ML";
-
+The ex subdirectory contains some examples.
Useful references on Constructive Type Theory:
@@ -29,4 +18,6 @@
Simon Thompson,
Type Theory and Functional Programming (Addison-Wesley, 1991)
-
+
+
+