| author | paulson |
| Thu, 18 Jan 1996 10:38:29 +0100 | |
| changeset 1444 | 23ceb1dc9755 |
| parent 1432 | 2cdb85e5cd90 |
| child 1518 | 03b770044429 |
| permissions | -rw-r--r-- |
<HTML><HEAD><TITLE>HOL/Lambda/ReadMe</TITLE></HEAD> <BODY> <H1>Lambda Calculus in de Bruijn's Notation</H1> This theory defines lambda-calculus terms with de Bruijn indixes and proves confluence of beta, eta and beta+eta. <P> A report describing the whole theory is found here: <A HREF = "ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/church-rosser.html" >More Church-Rosser Proofs (in Isabelle/HOL)</A>. </BODY> </HTML>