|
1269
|
1 |
(* Title: HOL/Lambda/ROOT.ML
|
|
1126
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
|
4 |
Copyright 1995 TUM
|
|
|
5 |
|
|
|
6 |
Confluence proof for untyped lambda-calculus using de Bruijn's notation.
|
|
1269
|
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
|
|
1126
|
11 |
|
|
|
12 |
@article{Takahashi-IC-95,author="Masako Takahashi",
|
|
|
13 |
title="Parallel Reductions in $\lambda$-Calculus",
|
|
|
14 |
journal=IC,year=1995,volume=118,pages="120--127"}
|
|
|
15 |
|
|
|
16 |
*)
|
|
|
17 |
|
|
1165
|
18 |
HOL_build_completed; (*Make examples fail if HOL did*)
|
|
1126
|
19 |
|
|
1165
|
20 |
writeln"Root file for HOL/Lambda";
|
|
1126
|
21 |
loadpath := [".","Lambda"];
|
|
1296
|
22 |
|
|
1269
|
23 |
time_use_thy "Eta";
|
|
1296
|
24 |
|
|
|
25 |
make_chart (); (*make HTML chart*)
|