src/HOL/Lambda/README.html
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2162 f53171d7f86c
child 8888 343c304e714a
permissions -rw-r--r--
Dep. on Provers/nat_transitive
     1 <!-- $Id$ -->
     2 <HTML><HEAD><TITLE>HOL/Lambda</TITLE></HEAD>
     3 <BODY>
     4 
     5 <H1>Lambda Calculus in de Bruijn's Notation</H1>
     6 
     7 This theory defines lambda-calculus terms with de Bruijn indixes and proves
     8 confluence of beta, eta and  beta+eta.
     9 <P>
    10 
    11 
    12 The paper
    13 <A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/ic.html">
    14 More Church-Rosser Proofs (in Isabelle/HOL)</A>
    15 describes the whole theory.
    16 
    17 <HR>
    18 
    19 <P>Last modified 5/11/96
    20 
    21 </BODY>
    22 </HTML>