--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Resid/README.html Tue Mar 05 17:23:21 1996 +0100
@@ -0,0 +1,28 @@
+<!-- $Id$ -->
+<HTML><HEAD><TITLE>HOL/Resid</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/Research/Reports/TR377-lcp-mechanising-set-theory.ps.gz">The Church-Rosser Theorem in Isabelle: A Proof Porting
+ Experiment</A>.
+
+<HR>
+
+<P>Last modified 5 March 1996