author | haftmann |
Tue, 18 Sep 2007 07:36:13 +0200 | |
changeset 24622 | 8116eb022282 |
parent 19336 | fb5e19d26d5e |
child 33615 | 261abc2e3155 |
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 Gerard Huet. Residual Theory in Lambda-Calculus: A Formal Development. J. Functional Programming 4(3) 1994, 371-394. *) time_use_thy "Confluence";