| author | paulson |
| Tue, 05 Mar 1996 16:27:01 +0100 | |
| changeset 1541 | c81c770f47ef |
| parent 1518 | 03b770044429 |
| child 1542 | 03e727af711d |
| permissions | -rw-r--r-- |
<HTML><HEAD><TITLE>HOL/Lambda</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> The report <A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/church-rosser.html"> More Church-Rosser Proofs (in Isabelle/HOL)</A> describes the whole theory. </BODY> </HTML>