# HG changeset patch
# User nipkow
# Date 816786960 -3600
# Node ID 8709e5aaefde15500123bb8ccf1b8671b3ef1e3d
# Parent d4e26f632bcab35906ca7de574d11bc0d628ba97
New README.html fuile
diff -r d4e26f632bca -r 8709e5aaefde src/HOL/Lambda/README.html
--- /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 @@
+HOL/Lambda/ReadMe
+
+
+Lambda Calculus in de Bruijn's Notation
+
+This theory defines lambda-calculus terms with de Bruijn indixes and proves
+confluence of beta, eta and beta+eta.
+
+Beta is proved confluent both in the traditional way (see Barendregt's book)
+and also following Takahashi's elegant version using developments.
+
+
+A report describing the whole theory with the exception of eta-reduction is
+found here: More Church-Rosser Proofs (in Isabelle).
+
+
+