author | wenzelm |
Thu, 11 Mar 1999 13:20:35 +0100 | |
changeset 6349 | f7750d816c21 |
parent 4446 | 097004a470fb |
child 9000 | c20d58286a51 |
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 |
||
6349
f7750d816c21
removed foo_build_completed -- now handled by session management (via usedir);
wenzelm
parents:
4446
diff
changeset
|
15 |
writeln"Root file for ZF/Resid"; |
1048 | 16 |
|
4446 | 17 |
set proof_timing; |
3733
1baedb1d4627
Previously loaded the WRONG THEORY, ignoring Confluence...
paulson
parents:
1461
diff
changeset
|
18 |
time_use_thy "Conversion"; |
1048 | 19 |
|
20 |
writeln"END: Root file for ZF/Resid"; |