src/Cube/README
author clasohm
Tue, 24 Oct 1995 14:45:35 +0100
changeset 1294 1358dc040edb
parent 0 a5a9c433f639
permissions -rw-r--r--
added calls of init_html and make_chart; added usage of qed
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
		Cube: Barendregt's Lambda-Cube
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
This directory contains the Standard ML sources of the Isabelle system for
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
the Lambda-Cube.  Important files include
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
ROOT.ML -- loads all source files.  Enter an ML image containing Pure
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
Isabelle and type: use "ROOT.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
Makefile -- compiles the files under Poly/ML or SML of New Jersey
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
ex.ML -- examples file.  To execute them, enter an ML image
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
containing Cube and type:    use "ex.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
NB: the formalization is not completely sound!  It does not enforce
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
distinctness of variable names in contexts!
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
For more information about the Lambda-Cube, see
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
	H. Barendregt
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
	Introduction to Generalised Type Systems
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
	J. Functional Programming
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21