--- a/src/HOL/BNF/README.html Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF/README.html Mon Jan 20 18:24:56 2014 +0100
@@ -30,9 +30,10 @@
</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.
+Most of the package is loaded as part of <tt>Main.thy</tt>. Additional
+functionality is provided by <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>