Minor mod.

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