equal
deleted
inserted
replaced
6 Executes the Residuals example. |
6 Executes the Residuals example. |
7 This is a proof of the Church-Rosser Theorem for the untyped lambda-calculus. |
7 This is a proof of the Church-Rosser Theorem for the untyped lambda-calculus. |
8 |
8 |
9 By Ole Rasmussen, following the Coq proof given in |
9 By Ole Rasmussen, following the Coq proof given in |
10 |
10 |
11 Gérard Huet. Residual Theory in Lambda-Calculus: A Formal Development. |
11 Gerard Huet. Residual Theory in Lambda-Calculus: A Formal Development. |
12 J. Functional Programming 4(3) 1994, 371-394. |
12 J. Functional Programming 4(3) 1994, 371-394. |
13 *) |
13 *) |
14 |
14 |
15 time_use_thy "Confluence"; |
15 time_use_thy "Confluence"; |