src/CTT/ROOT
changeset 51403 2ff3a5589b05
parent 51397 03b586ee5930
child 58974 cbc2ac19d783
--- a/src/CTT/ROOT	Tue Mar 12 20:03:04 2013 +0100
+++ b/src/CTT/ROOT	Tue Mar 12 21:59:48 2013 +0100
@@ -4,6 +4,17 @@
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
+
+    This is a version of Constructive Type Theory (extensional equality,
+    no universes).
+
+    Useful references on Constructive Type Theory:
+
+    B. Nordström, K. Petersson and J. M. Smith, Programming in Martin-Löf's
+    Type Theory (Oxford University Press, 1990)
+
+    Simon Thompson, Type Theory and Functional Programming (Addison-Wesley,
+    1991)
   *}
   options [document = false]
   theories Main