--- a/src/HOL/Codatatype/README.html Fri Sep 21 16:34:40 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,54 +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>BNF Package</title>
-</head>
-
-<body>
-
-<h3><i>BNF</i>: A (co)datatype package based on bounded natural functors
-(BNFs)</h3>
-
-<p>
-The <i>BNF</i> package provides a fully modular framework for constructing
-inductive and coinductive datatypes in HOL, with support for mixed mutual and
-nested (co)recursion. Mixed (co)recursion enables type definitions involving
-both datatypes and codatatypes, such as the type of finitely branching trees of
-possibly infinite depth. The framework draws heavily from category theory.
-
-<p>
-The package is described in the following paper:
-
-<ul>
- <li><a href="http://www21.in.tum.de/~traytel/papers/codatatypes/index.html">Foundational, Compositional (Co)datatypes for Higher-Order Logic—Category Theory Applied to Theorem Proving</a>, <br>
- Dmitriy Traytel, Andrei Popescu, and Jasmin Christian Blanchette.<br>
- <i>Logic in Computer Science (LICS 2012)</i>, 2012.
-</ul>
-
-<p>
-The main entry point for applications is <tt>BNF.thy</tt>. The <tt>Examples</tt>
-directory contains various examples of (co)datatypes, including the examples
-from the paper.
-
-<p>
-The key notion underlying the package is that of a <i>bounded natural functor</i>
-(<i>BNF</i>)—an enriched type constructor satisfying specific properties
-preserved by interesting categorical operations (composition, least fixed point,
-and greatest fixed point). The <tt>Basic_BNFs.thy</tt> and <tt>More_BNFs.thy</tt>
-files register various basic types, notably for sums, products, function spaces,
-finite sets, multisets, and countable sets. Custom BNFs can be registered as well.
-
-<p>
-<b>Warning:</b> The package is under development. Please contact any nonempty
-subset of
-<a href="mailto:traytel@in.tum.de">the</a>
-<a href="mailto:popescua@in.tum.de">above</a>
-<a href="mailto:blanchette@in.tum.de">authors</a>
-if you have questions or comments.
-
-</body>
-
-</html>