src/HOL/Lambda/ROOT.ML
author nipkow
Mon May 22 16:00:26 1995 +0200 (1995-05-22)
changeset 1126 50ac36140e21
child 1165 97b2bb5d43c3
permissions -rw-r--r--
Moved comment from ParRed.thy to ROOT.ML
     1 (*  Title: 	CHOL/IMP/ROOT.ML
     2     ID:         $Id$
     3     Author: 	Tobias Nipkow
     4     Copyright   1995 TUM
     5 
     6 Confluence proof for untyped lambda-calculus using de Bruijn's notation.
     7 Extremely slick proof; follows the first two pages of
     8 
     9 @article{Takahashi-IC-95,author="Masako Takahashi",
    10 title="Parallel Reductions in $\lambda$-Calculus",
    11 journal=IC,year=1995,volume=118,pages="120--127"}
    12 
    13 *)
    14 
    15 CHOL_build_completed;	(*Make examples fail if CHOL did*)
    16 
    17 writeln"Root file for CHOL/Lambda";
    18 loadpath := [".","Lambda"];
    19 time_use_thy "ParRed";