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