src/HOL/Lambda/README.html
author paulson
Tue, 05 Mar 1996 16:29:01 +0100
changeset 1542 03e727af711d
parent 1541 c81c770f47ef
child 1645 be85d119a805
permissions -rw-r--r--
Put quotes around URLs in links
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1542
03e727af711d Put quotes around URLs in links
paulson
parents: 1541
diff changeset
     1
<!-- $Id$ -->
1541
c81c770f47ef Put quotes around URLs in links
paulson
parents: 1518
diff changeset
     2
<HTML><HEAD><TITLE>HOL/Lambda</TITLE></HEAD>
1346
8709e5aaefde New README.html fuile
nipkow
parents:
diff changeset
     3
<BODY>
8709e5aaefde New README.html fuile
nipkow
parents:
diff changeset
     4
8709e5aaefde New README.html fuile
nipkow
parents:
diff changeset
     5
<H1>Lambda Calculus in de Bruijn's Notation</H1>
8709e5aaefde New README.html fuile
nipkow
parents:
diff changeset
     6
8709e5aaefde New README.html fuile
nipkow
parents:
diff changeset
     7
This theory defines lambda-calculus terms with de Bruijn indixes and proves
8709e5aaefde New README.html fuile
nipkow
parents:
diff changeset
     8
confluence of beta, eta and  beta+eta.
8709e5aaefde New README.html fuile
nipkow
parents:
diff changeset
     9
<P>
1432
2cdb85e5cd90 Minor mod.
nipkow
parents: 1346
diff changeset
    10
1346
8709e5aaefde New README.html fuile
nipkow
parents:
diff changeset
    11
1541
c81c770f47ef Put quotes around URLs in links
paulson
parents: 1518
diff changeset
    12
The report 
c81c770f47ef Put quotes around URLs in links
paulson
parents: 1518
diff changeset
    13
<A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/church-rosser.html">
c81c770f47ef Put quotes around URLs in links
paulson
parents: 1518
diff changeset
    14
More Church-Rosser Proofs (in Isabelle/HOL)</A>
c81c770f47ef Put quotes around URLs in links
paulson
parents: 1518
diff changeset
    15
describes the whole theory.
1346
8709e5aaefde New README.html fuile
nipkow
parents:
diff changeset
    16
1542
03e727af711d Put quotes around URLs in links
paulson
parents: 1541
diff changeset
    17
<HR>
03e727af711d Put quotes around URLs in links
paulson
parents: 1541
diff changeset
    18
03e727af711d Put quotes around URLs in links
paulson
parents: 1541
diff changeset
    19
<P>Last modified 5 March 1996
03e727af711d Put quotes around URLs in links
paulson
parents: 1541
diff changeset
    20
1346
8709e5aaefde New README.html fuile
nipkow
parents:
diff changeset
    21
</BODY>
8709e5aaefde New README.html fuile
nipkow
parents:
diff changeset
    22
</HTML>