src/CTT/README
author paulson
Tue Apr 30 11:08:09 1996 +0200 (1996-04-30)
changeset 1702 4aa538e82f76
parent 0 a5a9c433f639
permissions -rw-r--r--
Cosmetic re-ordering of declarations
     1 		CTT: Constructive Type Theory
     2 
     3 This directory contains the Standard ML sources of the Isabelle system for
     4 Constructive Type Theory (extensional equality, no universes).  Important
     5 files include
     6 
     7 ROOT.ML -- loads all source files.  Enter an ML image containing Pure
     8 Isabelle and type:    use "ROOT.ML";
     9 
    10 Makefile -- compiles the files under Poly/ML or SML of New Jersey
    11 
    12 ex -- subdirectory containing examples.  To execute them, enter an ML image
    13 containing CTT and type:    use "ex/ROOT.ML";
    14 
    15 Useful references on Constructive Type Theory:
    16 
    17 	B. Nordstr\"om, K. Petersson and J. M. Smith,
    18 	Programming in Martin-L\"of's Type Theory
    19 	(Oxford University Press, 1990)
    20 
    21 	Simon Thompson,
    22 	Type Theory and Functional Programming (Addison-Wesley, 1991)
    23