# HG changeset patch
# User paulson
# Date 844861658 -7200
# Node ID 8f0d199373a3700b7847a2f1bfe006c2518486ab
# Parent  b198b3d46fb421a11cdef0fd3f1d53cc6ab0b79d
Plain text README files now redundant due to HTML versions

diff -r b198b3d46fb4 -r 8f0d199373a3 src/CTT/README
--- a/src/CTT/README	Wed Oct 09 13:43:51 1996 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-		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)
-