equal
deleted
inserted
replaced
1 (* Title: HOL/IMP/ROOT.ML |
1 (* Title: HOL/Lambda/ROOT.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1995 TUM |
4 Copyright 1995 TUM |
5 |
5 |
6 Confluence proof for untyped lambda-calculus using de Bruijn's notation. |
6 Confluence proof for untyped lambda-calculus using de Bruijn's notation. |
7 Extremely slick proof; follows the first two pages of |
7 Covers beta, eta, and beta+eta. |
|
8 |
|
9 Beta is proved confluent both in the traditional way and also following the |
|
10 first two pages of |
8 |
11 |
9 @article{Takahashi-IC-95,author="Masako Takahashi", |
12 @article{Takahashi-IC-95,author="Masako Takahashi", |
10 title="Parallel Reductions in $\lambda$-Calculus", |
13 title="Parallel Reductions in $\lambda$-Calculus", |
11 journal=IC,year=1995,volume=118,pages="120--127"} |
14 journal=IC,year=1995,volume=118,pages="120--127"} |
12 |
15 |
14 |
17 |
15 HOL_build_completed; (*Make examples fail if HOL did*) |
18 HOL_build_completed; (*Make examples fail if HOL did*) |
16 |
19 |
17 writeln"Root file for HOL/Lambda"; |
20 writeln"Root file for HOL/Lambda"; |
18 loadpath := [".","Lambda"]; |
21 loadpath := [".","Lambda"]; |
19 time_use_thy "ParRed"; |
22 time_use_thy "Eta"; |