--- a/src/ZF/Coind/README.html Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +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/Coind/README</TITLE>
-</HEAD>
-
-<BODY>
-
-<H2>Coind -- A Coinduction Example</H2>
-
-Jacob Frost has mechanized the proofs from the article
-
-<P>
-<PRE>
-@Article{milner-coind,
- author = "Robin Milner and Mads Tofte",
- title = "Co-induction in Relational Semantics",
- journal = TCS,
- year = 1991,
- volume = 87,
- pages = "209--220"}
-</PRE>
-
-<P> It involves proving the consistency of the dynamic and static semantics
-for a small functional language. A codatatype definition specifies values and
-value environments in mutual recursion: non-well-founded values represent
-recursive functions; value environments are variant functions from variables
-into values.
-
-<P>
-Frost's
-<A
-HREF="http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz">report</A> describes this development.
-
-</body>
-</html>