--- a/src/ZF/Resid/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/ZF/Resid/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,29 +1,36 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- $Id$ -->
-<HTML><HEAD><TITLE>ZF/Resid/README</TITLE></HEAD><BODY>
+
+<html>
-<H2>Resid -- A theory of residuals</H2>
+<head>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <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>
+<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>
+ 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>.
+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>