Fixed the treatment of substitution for equations, restricting occurrences of
variables on the RHS. Improves performance in many cases, though a few old
proofs fail
<!-- $Id$ -->
<HTML><HEAD><TITLE>ZF/Resid/README</TITLE></HEAD><BODY>
<H2>Resid -- A theory of residuals</H2>
Ole Rasmussen has ported to Isabelle/ZF the Coq proofs described in the
article
<P>
<PRE>
@Article{huet-residual,
author = "{G\'erard} Huet",
title = "Residual Theory in $\lambda$-Calculus: A Formal
Development",
journal = JFP,
year = 1994,
volume = 4,
number = 3,
pages = "371--394"}
</PRE>
See Rasmussen's report
<A HREF="http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz">The Church-Rosser Theorem in Isabelle: A Proof Porting
Experiment</A>.
</body>
</html>