# HG changeset patch
# User nipkow
# Date 816787051 -3600
# Node ID 89550840ef93b3dad1eb8eb36ae7d1e1ea67e1ed
# Parent  8709e5aaefde15500123bb8ccf1b8671b3ef1e3d
Moved comments into README.html

diff -r 8709e5aaefde -r 89550840ef93 src/HOL/Lambda/ROOT.ML
--- a/src/HOL/Lambda/ROOT.ML	Sun Nov 19 14:16:00 1995 +0100
+++ b/src/HOL/Lambda/ROOT.ML	Sun Nov 19 14:17:31 1995 +0100
@@ -2,17 +2,6 @@
     ID:         $Id$
     Author: 	Tobias Nipkow
     Copyright   1995 TUM
-
-Confluence proof for untyped lambda-calculus using de Bruijn's notation.
-Covers beta, eta, and beta+eta.
-
-Beta is proved confluent both in the traditional way and also following the
-first two pages of
-
-@article{Takahashi-IC-95,author="Masako Takahashi",
-title="Parallel Reductions in $\lambda$-Calculus",
-journal=IC,year=1995,volume=118,pages="120--127"}
-
 *)
 
 HOL_build_completed;	(*Make examples fail if HOL did*)