src/HOL/Lambda/ROOT.ML
changeset 1347 89550840ef93
parent 1296 ae31bb7774a7
child 1351 4a960c012383
     1.1 --- a/src/HOL/Lambda/ROOT.ML	Sun Nov 19 14:16:00 1995 +0100
     1.2 +++ b/src/HOL/Lambda/ROOT.ML	Sun Nov 19 14:17:31 1995 +0100
     1.3 @@ -2,17 +2,6 @@
     1.4      ID:         $Id$
     1.5      Author: 	Tobias Nipkow
     1.6      Copyright   1995 TUM
     1.7 -
     1.8 -Confluence proof for untyped lambda-calculus using de Bruijn's notation.
     1.9 -Covers beta, eta, and beta+eta.
    1.10 -
    1.11 -Beta is proved confluent both in the traditional way and also following the
    1.12 -first two pages of
    1.13 -
    1.14 -@article{Takahashi-IC-95,author="Masako Takahashi",
    1.15 -title="Parallel Reductions in $\lambda$-Calculus",
    1.16 -journal=IC,year=1995,volume=118,pages="120--127"}
    1.17 -
    1.18  *)
    1.19  
    1.20  HOL_build_completed;	(*Make examples fail if HOL did*)