src/HOL/Lambda/ROOT.ML
author clasohm
Thu Jun 29 12:48:48 1995 +0200 (1995-06-29)
changeset 1165 97b2bb5d43c3
parent 1126 50ac36140e21
child 1269 ee011b365770
permissions -rw-r--r--
renamed CHOL to HOL
     1 (*  Title: 	HOL/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 HOL_build_completed;	(*Make examples fail if HOL did*)
    16 
    17 writeln"Root file for HOL/Lambda";
    18 loadpath := [".","Lambda"];
    19 time_use_thy "ParRed";