author | wenzelm |
Wed, 15 Oct 1997 15:12:59 +0200 | |
changeset 3872 | a5839ecee7b8 |
parent 3733 | 1baedb1d4627 |
child 4446 | 097004a470fb |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/Resid/ROOT |
1048 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
1048 | 4 |
Copyright 1995 University of Cambridge |
5 |
||
6 |
Executes the Residuals example. |
|
7 |
This is a proof of the Church-Rosser Theorem for the untyped lambda-calculus. |
|
8 |
||
9 |
By Ole Rasmussen, following the Coq proof given in |
|
10 |
||
11 |
Gérard Huet. Residual Theory in Lambda-Calculus: A Formal Development. |
|
12 |
J. Functional Programming 4(3) 1994, 371-394. |
|
13 |
*) |
|
14 |
||
1461 | 15 |
ZF_build_completed; (*Make examples fail if ZF did*) |
1048 | 16 |
|
17 |
writeln"Root file for ZF/Resid"; |
|
18 |
proof_timing := true; |
|
19 |
||
3733
1baedb1d4627
Previously loaded the WRONG THEORY, ignoring Confluence...
paulson
parents:
1461
diff
changeset
|
20 |
time_use_thy "Conversion"; |
1048 | 21 |
|
22 |
writeln"END: Root file for ZF/Resid"; |