Minor mod.
Sat, 06 Jan 1996 14:02:52 +0100
changeset 1432 2cdb85e5cd90
parent 1431 be7c6d77e19c
child 1433 e7f9273024c2
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.
-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: <A HREF =
+A report describing the whole theory is found here: <A HREF =
->More Church-Rosser Proofs (in Isabelle)</A>.
+>More Church-Rosser Proofs (in Isabelle/HOL)</A>.