src/HOL/Proofs/Lambda/README.html
changeset 39157 b98909faaea8
parent 36862 952b2b102a0a
equal deleted inserted replaced
39156:b4f18ac786fa 39157:b98909faaea8
       
     1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
       
     2 
       
     3 <HTML>
       
     4 
       
     5 <HEAD>
       
     6   <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
       
     7   <TITLE>HOL/Lambda</TITLE>
       
     8 </HEAD>
       
     9 
       
    10 <BODY>
       
    11 
       
    12 <H1>Lambda Calculus in de Bruijn's Notation</H1>
       
    13 
       
    14 This theory defines lambda-calculus terms with de Bruijn indixes and proves
       
    15 confluence of beta, eta and  beta+eta.
       
    16 <P>
       
    17 
       
    18 
       
    19 The paper
       
    20 <A HREF="http://www.in.tum.de/~nipkow/pubs/jar2001.html">
       
    21 More Church-Rosser Proofs (in Isabelle/HOL)</A>
       
    22 describes the whole theory.
       
    23 
       
    24 <HR>
       
    25 
       
    26 <P>Last modified 20.5.2000
       
    27 
       
    28 </BODY>
       
    29 </HTML>