src/HOL/Lambda/README.html
author haftmann
Wed, 20 May 2009 10:37:37 +0200
changeset 31207 7eb05fc49b45
parent 15582 7219facb3fd0
child 36862 952b2b102a0a
permissions -rw-r--r--
added generator for type copies (records)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15283
f21466450330 DOCTYPE declaration added
webertj
parents: 13360
diff changeset
     1
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
f21466450330 DOCTYPE declaration added
webertj
parents: 13360
diff changeset
     2
1542
03e727af711d Put quotes around URLs in links
paulson
parents: 1541
diff changeset
     3
<!-- $Id$ -->
15582
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     4
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     5
<HTML>
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     6
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     7
<HEAD>
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     8
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     9
  <TITLE>HOL/Lambda</TITLE>
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
    10
</HEAD>
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
    11
1346
8709e5aaefde New README.html fuile
nipkow
parents:
diff changeset
    12
<BODY>
8709e5aaefde New README.html fuile
nipkow
parents:
diff changeset
    13
8709e5aaefde New README.html fuile
nipkow
parents:
diff changeset
    14
<H1>Lambda Calculus in de Bruijn's Notation</H1>
8709e5aaefde New README.html fuile
nipkow
parents:
diff changeset
    15
8709e5aaefde New README.html fuile
nipkow
parents:
diff changeset
    16
This theory defines lambda-calculus terms with de Bruijn indixes and proves
8709e5aaefde New README.html fuile
nipkow
parents:
diff changeset
    17
confluence of beta, eta and  beta+eta.
8709e5aaefde New README.html fuile
nipkow
parents:
diff changeset
    18
<P>
1432
2cdb85e5cd90 Minor mod.
nipkow
parents: 1346
diff changeset
    19
1346
8709e5aaefde New README.html fuile
nipkow
parents:
diff changeset
    20
1645
be85d119a805 Moved link to paper.
nipkow
parents: 1542
diff changeset
    21
The paper
13360
ece4b151f963 *** empty log message ***
nipkow
parents: 8888
diff changeset
    22
<A HREF="http://www.in.tum.de/~nipkow/pubs/jar2001.html">
1541
c81c770f47ef Put quotes around URLs in links
paulson
parents: 1518
diff changeset
    23
More Church-Rosser Proofs (in Isabelle/HOL)</A>
c81c770f47ef Put quotes around URLs in links
paulson
parents: 1518
diff changeset
    24
describes the whole theory.
1346
8709e5aaefde New README.html fuile
nipkow
parents:
diff changeset
    25
1542
03e727af711d Put quotes around URLs in links
paulson
parents: 1541
diff changeset
    26
<HR>
03e727af711d Put quotes around URLs in links
paulson
parents: 1541
diff changeset
    27
8888
343c304e714a fixed link
nipkow
parents: 2162
diff changeset
    28
<P>Last modified 20.5.2000
1542
03e727af711d Put quotes around URLs in links
paulson
parents: 1541
diff changeset
    29
1346
8709e5aaefde New README.html fuile
nipkow
parents:
diff changeset
    30
</BODY>
8709e5aaefde New README.html fuile
nipkow
parents:
diff changeset
    31
</HTML>