src/Cube/README.html
author nipkow
Tue, 17 Oct 2000 08:00:46 +0200
changeset 10228 e653cb933293
parent 3279 815ef5848324
child 15283 f21466450330
permissions -rw-r--r--
added intermediate value thms
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 1341
diff changeset
     1
815ef5848324 tuned all READMEs;
wenzelm
parents: 1341
diff changeset
     2
<HTML><HEAD><TITLE>Cube/README</TITLE></HEAD><BODY>
1341
69fec018854c HTML version of README
clasohm
parents:
diff changeset
     3
69fec018854c HTML version of README
clasohm
parents:
diff changeset
     4
<H2>Cube: Barendregt's Lambda-Cube</H2>
69fec018854c HTML version of README
clasohm
parents:
diff changeset
     5
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 1341
diff changeset
     6
This directory contains the ML sources of the Isabelle system for the
815ef5848324 tuned all READMEs;
wenzelm
parents: 1341
diff changeset
     7
Lambda-Cube.<p>
1341
69fec018854c HTML version of README
clasohm
parents:
diff changeset
     8
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 1341
diff changeset
     9
The <tt>ex</tt> subdirectory contains some examples.<p>
1341
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    10
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    11
NB: the formalization is not completely sound!  It does not enforce
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    12
distinctness of variable names in contexts!<P>
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    13
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    14
For more information about the Lambda-Cube, see
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    15
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    16
<UL>
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    17
<LI>H. Barendregt<BR>
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    18
    Introduction to Generalised Type Systems<BR>
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    19
    J. Functional Programming
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    20
</UL>
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 1341
diff changeset
    21
</BODY>
815ef5848324 tuned all READMEs;
wenzelm
parents: 1341
diff changeset
    22
</HTML>