author | wenzelm |
Tue, 30 May 2000 16:08:38 +0200 | |
changeset 9000 | c20d58286a51 |
parent 6349 | f7750d816c21 |
child 12593 | cd35fe5947d4 |
permissions | -rw-r--r-- |
(* Title: ZF/Resid/ROOT ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1995 University of Cambridge Executes the Residuals example. This is a proof of the Church-Rosser Theorem for the untyped lambda-calculus. By Ole Rasmussen, following the Coq proof given in Gérard Huet. Residual Theory in Lambda-Calculus: A Formal Development. J. Functional Programming 4(3) 1994, 371-394. *) time_use_thy "Conversion";