| author | paulson |
| Mon, 23 Sep 1996 17:42:56 +0200 | |
| changeset 2003 | b48f066d52dc |
| parent 1645 | be85d119a805 |
| child 2162 | f53171d7f86c |
| 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://www4.informatik.tu-muenchen.de/~nipkow/pubs/cade96.html"> More Church-Rosser Proofs (in Isabelle/HOL)</A> describes the whole theory. <HR> <P>Last modified 4 April 1996 </BODY> </HTML>