Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Lambda/README.html
author paulson
Tue, 21 Sep 1999 11:11:09 +0200
changeset 7547 a72a551b6d79
parent 2162 f53171d7f86c
child 8888 343c304e714a
permissions -rw-r--r--
new proof of drop_prog_correct for new definition of project_act

<!-- $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/ic.html">
More Church-Rosser Proofs (in Isabelle/HOL)</A>
describes the whole theory.

<HR>

<P>Last modified 5/11/96

</BODY>
</HTML>
isabelle