equal
deleted
inserted
replaced
1 (* Title: CHOL/IMP/ROOT.ML |
1 (* Title: HOL/IMP/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. |
10 title="Parallel Reductions in $\lambda$-Calculus", |
10 title="Parallel Reductions in $\lambda$-Calculus", |
11 journal=IC,year=1995,volume=118,pages="120--127"} |
11 journal=IC,year=1995,volume=118,pages="120--127"} |
12 |
12 |
13 *) |
13 *) |
14 |
14 |
15 CHOL_build_completed; (*Make examples fail if CHOL did*) |
15 HOL_build_completed; (*Make examples fail if HOL did*) |
16 |
16 |
17 writeln"Root file for CHOL/Lambda"; |
17 writeln"Root file for HOL/Lambda"; |
18 loadpath := [".","Lambda"]; |
18 loadpath := [".","Lambda"]; |
19 time_use_thy "ParRed"; |
19 time_use_thy "ParRed"; |