src/CTT/README

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/CTT/README	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,23 @@
+		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
+
+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";
+
+Useful references on Constructive Type Theory:
+
+	B. Nordstr\"om, K. Petersson and J. M. Smith,
+	Programming in Martin-L\"of's Type Theory
+	(Oxford University Press, 1990)
+
+	Simon Thompson,
+	Type Theory and Functional Programming (Addison-Wesley, 1991)
+