src/CTT/README.html
changeset 19761 5cd82054c2c6
parent 15582 7219facb3fd0
child 19762 957bcf55c98f
equal deleted inserted replaced
19760:c7e9cc10acc8 19761:5cd82054c2c6
    11 
    11 
    12 <BODY>
    12 <BODY>
    13 
    13 
    14 <H2>CTT: Constructive Type Theory</H2>
    14 <H2>CTT: Constructive Type Theory</H2>
    15 
    15 
    16 This directory contains the ML sources of the Isabelle system for
    16 This is a version of Constructive Type Theory (extensional equality, no universes).<p>
    17 Constructive Type Theory (extensional equality, no universes).<p>
       
    18 
       
    19 The <tt>ex</tt> subdirectory contains some examples.<p>
       
    20 
    17 
    21 Useful references on Constructive Type Theory:
    18 Useful references on Constructive Type Theory:
    22 
    19 
    23 <UL>
    20 <UL>
    24 <LI>	B. Nordstrm, K. Petersson and J. M. Smith,<BR>
    21 <LI>	B. Nordstrm, K. Petersson and J. M. Smith,<BR>