<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>

<!-- $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 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.

<HR>

<P>Last modified 5 March 1996

</BODY>
</HTML>

Put quotes around URLs in links
Put quotes around URLs in links
