src/CTT/README.html
changeset 1341 69fec018854c
child 3279 815ef5848324
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/CTT/README.html	Fri Nov 17 13:22:50 1995 +0100
     1.3 @@ -0,0 +1,32 @@
     1.4 +<HTML><HEAD><TITLE>CTT/ReadMe</TITLE></HEAD><BODY>
     1.5 +
     1.6 +<H2>CTT: Constructive Type Theory</H2>
     1.7 +
     1.8 +This directory contains the Standard ML sources of the Isabelle system for
     1.9 +Constructive Type Theory (extensional equality, no universes).  Important
    1.10 +files include
    1.11 +
    1.12 +<DL>
    1.13 +<DT>ROOT.ML
    1.14 +<DD>loads all source files.  Enter an ML image containing Pure
    1.15 +Isabelle and type: use "ROOT.ML";<P>
    1.16 +
    1.17 +<DT>Makefile
    1.18 +<DD>compiles the files under Poly/ML or SML of New Jersey<P>
    1.19 +
    1.20 +<DT>ex
    1.21 +<DD>subdirectory containing examples.  To execute them, enter an ML image
    1.22 +containing CTT and type: use "ex/ROOT.ML";<P>
    1.23 +</DL>
    1.24 +
    1.25 +Useful references on Constructive Type Theory:
    1.26 +
    1.27 +<UL>
    1.28 +<LI>	B. Nordström, K. Petersson and J. M. Smith,<BR>
    1.29 +	Programming in Martin-Löf's Type Theory<BR>
    1.30 +	(Oxford University Press, 1990)
    1.31 +
    1.32 +<LI>	Simon Thompson,<BR>
    1.33 +	Type Theory and Functional Programming (Addison-Wesley, 1991)
    1.34 +</UL>
    1.35 +</BODY></HTML>