author | wenzelm |
Tue, 24 Jul 2012 21:36:53 +0200 | |
changeset 48487 | 94a9650f79fb |
parent 33615 | 261abc2e3155 |
permissions | -rw-r--r-- |
(* Title: ZF/Resid/ROOT.ML 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. *) use_thys ["Confluence"];