author | nipkow |
Mon, 02 Mar 2009 16:53:55 +0100 | |
changeset 30198 | 922f944f03b2 |
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";