author | wenzelm |
Sun, 30 Jan 2011 13:02:18 +0100 | |
changeset 41648 | 6d736d983d5c |
parent 33615 | 261abc2e3155 |
permissions | -rw-r--r-- |
33615 | 1 |
(* Title: ZF/Resid/ROOT.ML |
1461 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
1048 | 3 |
Copyright 1995 University of Cambridge |
4 |
||
5 |
Executes the Residuals example. |
|
6 |
This is a proof of the Church-Rosser Theorem for the untyped lambda-calculus. |
|
7 |
||
8 |
By Ole Rasmussen, following the Coq proof given in |
|
9 |
||
19336
fb5e19d26d5e
removed some illegal characters: they were crashing SML/NJ
paulson
parents:
12593
diff
changeset
|
10 |
Gerard Huet. Residual Theory in Lambda-Calculus: A Formal Development. |
1048 | 11 |
J. Functional Programming 4(3) 1994, 371-394. |
12 |
*) |
|
13 |
||
33615 | 14 |
use_thys ["Confluence"]; |