author | wenzelm |
Thu, 06 Dec 2001 00:39:40 +0100 | |
changeset 12397 | 6766aa05e4eb |
parent 8888 | 343c304e714a |
child 13360 | ece4b151f963 |
permissions | -rw-r--r-- |
<!-- $Id$ --> <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 paper <A HREF="http://www.in.tum.de/~nipkow/pubs/jar2000.html"> More Church-Rosser Proofs (in Isabelle/HOL)</A> describes the whole theory. <HR> <P>Last modified 20.5.2000 </BODY> </HTML>