src/Cube/README.html
author wenzelm
Fri, 17 Aug 2012 11:23:57 +0200
changeset 48835 574042d14fd9
parent 36862 952b2b102a0a
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15283
f21466450330 DOCTYPE declaration added
webertj
parents: 3279
diff changeset
     1
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 1341
diff changeset
     2
15582
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     3
<HTML>
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     4
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     5
<HEAD>
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     6
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     7
  <TITLE>Cube/README</TITLE>
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     8
</HEAD>
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     9
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
    10
<BODY>
1341
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    11
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    12
<H2>Cube: Barendregt's Lambda-Cube</H2>
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    13
17254
wenzelm
parents: 15582
diff changeset
    14
This directory contains the theory sources for the Lambda-Cube in
wenzelm
parents: 15582
diff changeset
    15
Isabelle/Pure.<p>
1341
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    16
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 1341
diff changeset
    17
The <tt>ex</tt> subdirectory contains some examples.<p>
1341
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    18
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    19
NB: the formalization is not completely sound!  It does not enforce
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    20
distinctness of variable names in contexts!<P>
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    21
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    22
For more information about the Lambda-Cube, see
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>H. Barendregt<BR>
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    26
    Introduction to Generalised Type Systems<BR>
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    27
    J. Functional Programming
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    28
</UL>
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 1341
diff changeset
    29
</BODY>
815ef5848324 tuned all READMEs;
wenzelm
parents: 1341
diff changeset
    30
</HTML>