author | paulson |
Fri, 31 Mar 2006 10:53:33 +0200 | |
changeset 19336 | fb5e19d26d5e |
parent 12593 | cd35fe5947d4 |
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";