src/CTT/README.html
author paulson
Tue Apr 30 11:08:09 1996 +0200 (1996-04-30)
changeset 1702 4aa538e82f76
parent 1341 69fec018854c
child 3279 815ef5848324
permissions -rw-r--r--
Cosmetic re-ordering of declarations
     1 <HTML><HEAD><TITLE>CTT/ReadMe</TITLE></HEAD><BODY>
     2 
     3 <H2>CTT: Constructive Type Theory</H2>
     4 
     5 This directory contains the Standard ML sources of the Isabelle system for
     6 Constructive Type Theory (extensional equality, no universes).  Important
     7 files include
     8 
     9 <DL>
    10 <DT>ROOT.ML
    11 <DD>loads all source files.  Enter an ML image containing Pure
    12 Isabelle and type: use "ROOT.ML";<P>
    13 
    14 <DT>Makefile
    15 <DD>compiles the files under Poly/ML or SML of New Jersey<P>
    16 
    17 <DT>ex
    18 <DD>subdirectory containing examples.  To execute them, enter an ML image
    19 containing CTT and type: use "ex/ROOT.ML";<P>
    20 </DL>
    21 
    22 Useful references on Constructive Type Theory:
    23 
    24 <UL>
    25 <LI>	B. Nordström, K. Petersson and J. M. Smith,<BR>
    26 	Programming in Martin-Löf's Type Theory<BR>
    27 	(Oxford University Press, 1990)
    28 
    29 <LI>	Simon Thompson,<BR>
    30 	Type Theory and Functional Programming (Addison-Wesley, 1991)
    31 </UL>
    32 </BODY></HTML>