--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lambda/README.html Sun Nov 19 14:16:00 1995 +0100
@@ -0,0 +1,19 @@
+<HTML><HEAD><TITLE>HOL/Lambda/ReadMe</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>
+Beta is proved confluent both in the traditional way (see Barendregt's book)
+and also following Takahashi's elegant version using developments.
+<P>
+
+A report describing the whole theory with the exception of eta-reduction is
+found here: <A HREF =
+"ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/church-rosser.html"
+>More Church-Rosser Proofs (in Isabelle)</A>.
+
+</BODY>
+</HTML>