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