# HG changeset patch
# User nipkow
# Date 820933372 -3600
# Node ID 2cdb85e5cd90ed8103757bc2d58bb8704445ca5a
# Parent  be7c6d77e19ccc52989f4276234a9140bb44bb3c
Minor mod.

diff -r be7c6d77e19c -r 2cdb85e5cd90 src/HOL/Lambda/README.html
--- a/src/HOL/Lambda/README.html	Tue Jan 02 14:08:04 1996 +0100
+++ b/src/HOL/Lambda/README.html	Sat Jan 06 14:02:52 1996 +0100
@@ -6,14 +6,11 @@
 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 =
+A report describing the whole theory is found here: <A HREF =
 "ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/church-rosser.html"
->More Church-Rosser Proofs (in Isabelle)</A>.
+>More Church-Rosser Proofs (in Isabelle/HOL)</A>.
 
 </BODY>
 </HTML>