--- a/src/ZF/Resid/README.html Tue Mar 12 19:55:17 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-
-<html>
-
-<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>
-@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>