src/HOL/Lambda/ROOT.ML
changeset 1269 ee011b365770
parent 1165 97b2bb5d43c3
child 1296 ae31bb7774a7
     1.1 --- a/src/HOL/Lambda/ROOT.ML	Thu Oct 05 14:45:54 1995 +0100
     1.2 +++ b/src/HOL/Lambda/ROOT.ML	Fri Oct 06 10:45:11 1995 +0100
     1.3 @@ -1,10 +1,13 @@
     1.4 -(*  Title: 	HOL/IMP/ROOT.ML
     1.5 +(*  Title: 	HOL/Lambda/ROOT.ML
     1.6      ID:         $Id$
     1.7      Author: 	Tobias Nipkow
     1.8      Copyright   1995 TUM
     1.9  
    1.10  Confluence proof for untyped lambda-calculus using de Bruijn's notation.
    1.11 -Extremely slick proof; follows the first two pages of
    1.12 +Covers beta, eta, and beta+eta.
    1.13 +
    1.14 +Beta is proved confluent both in the traditional way and also following the
    1.15 +first two pages of
    1.16  
    1.17  @article{Takahashi-IC-95,author="Masako Takahashi",
    1.18  title="Parallel Reductions in $\lambda$-Calculus",
    1.19 @@ -16,4 +19,4 @@
    1.20  
    1.21  writeln"Root file for HOL/Lambda";
    1.22  loadpath := [".","Lambda"];
    1.23 -time_use_thy "ParRed";
    1.24 +time_use_thy "Eta";