--- a/src/HOL/Lambda/ROOT.ML Thu Oct 05 14:45:54 1995 +0100
+++ b/src/HOL/Lambda/ROOT.ML Fri Oct 06 10:45:11 1995 +0100
@@ -1,10 +1,13 @@
-(* Title: HOL/IMP/ROOT.ML
+(* Title: HOL/Lambda/ROOT.ML
ID: $Id$
Author: Tobias Nipkow
Copyright 1995 TUM
Confluence proof for untyped lambda-calculus using de Bruijn's notation.
-Extremely slick proof; follows the first two pages of
+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",
@@ -16,4 +19,4 @@
writeln"Root file for HOL/Lambda";
loadpath := [".","Lambda"];
-time_use_thy "ParRed";
+time_use_thy "Eta";