src/HOL/Lambda/README.html
changeset 1645 be85d119a805
parent 1542 03e727af711d
child 2162 f53171d7f86c
equal deleted inserted replaced
1644:681f70ca3cf7 1645:be85d119a805
     7 This theory defines lambda-calculus terms with de Bruijn indixes and proves
     7 This theory defines lambda-calculus terms with de Bruijn indixes and proves
     8 confluence of beta, eta and  beta+eta.
     8 confluence of beta, eta and  beta+eta.
     9 <P>
     9 <P>
    10 
    10 
    11 
    11 
    12 The report 
    12 The paper
    13 <A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/church-rosser.html">
    13 <A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/cade96.html">
    14 More Church-Rosser Proofs (in Isabelle/HOL)</A>
    14 More Church-Rosser Proofs (in Isabelle/HOL)</A>
    15 describes the whole theory.
    15 describes the whole theory.
    16 
    16 
    17 <HR>
    17 <HR>
    18 
    18 
    19 <P>Last modified 5 March 1996
    19 <P>Last modified 4 April 1996
    20 
    20 
    21 </BODY>
    21 </BODY>
    22 </HTML>
    22 </HTML>