diff -r c7e9cc10acc8 -r 5cd82054c2c6 src/CTT/README.html --- a/src/CTT/README.html Fri Jun 02 16:06:19 2006 +0200 +++ b/src/CTT/README.html Fri Jun 02 18:15:38 2006 +0200 @@ -13,10 +13,7 @@

CTT: Constructive Type Theory

-This directory contains the ML sources of the Isabelle system for -Constructive Type Theory (extensional equality, no universes).

- -The ex subdirectory contains some examples.

+This is a version of Constructive Type Theory (extensional equality, no universes).

Useful references on Constructive Type Theory: