--- a/src/HOL/Codatatype/README.html Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/README.html Fri Sep 21 16:34:40 2012 +0200
@@ -4,21 +4,20 @@
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
- <title>Codatatype Package</title>
+ <title>BNF Package</title>
</head>
<body>
-<h3><i>Codatatype</i>: A (co)datatype package based on bounded natural functors
+<h3><i>BNF</i>: A (co)datatype package based on bounded natural functors
(BNFs)</h3>
<p>
-The <i>Codatatype</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.
+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:
@@ -30,24 +29,21 @@
</ul>
<p>
-The main entry point for applications is <tt>Codatatype.thy</tt>.
-The <tt>Examples</tt> directory contains various examples of (co)datatypes,
-including the examples from the paper.
+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> file registers
-various basic types, notably for sums, products, function spaces, finite sets,
-multisets, and countable sets. Custom BNFs can be registered as well.
+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. Future versions are expected
-to support multiple constructors and selectors per (co)datatype (instead of a
-single <i>fld</i> or <i>unf</i> constant) and provide a nicer syntax for
-(co)induction and (co)recursive function definitions. Please contact
-any nonempty subset of
+<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>