# HG changeset patch
# User blanchet
# Date 1375389424 -7200
# Node ID 591e76f2651e09082fb78ededf1ca1107a517bcf
# Parent  e1c6fa322d961451cf0a30a222deee891d0512d8
minor doc fixes

diff -r e1c6fa322d96 -r 591e76f2651e src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Thu Aug 01 22:28:49 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Aug 01 22:37:04 2013 +0200
@@ -705,6 +705,9 @@
 This section explains how to set up the (co)datatype package to allow nested
 recursion through custom well-behaved type constructors. The key concept is that
 of a bounded natural functor (BNF).
+
+    * @{command bnf}
+    * @{command print_bnfs}
 *}
 
 
@@ -736,6 +739,9 @@
 
   * also useful for compatibility with old package, e.g. add destructors to
     old @{command datatype}
+
+  * @{command wrap_free_constructors}
+    * \keyw{no\_dests}, \keyw{rep\_compat}
 *}
 
 
@@ -816,13 +822,13 @@
   \label{sec:acknowledgments} *}
 
 text {*
-Tobias Nipkow and Makarius Wenzel have made this work possible. Andreas
-Lochbihler has provided lots of comments on earlier versions of the package,
-especially for the coinductive part. Brian Huffman suggested major
-simplifications to the internal constructions, much of which has yet to be
-implemented. Stefan Milius and Lutz Schr\"oder suggested an elegant prove to
-eliminate one of the BNF assumptions. Florian Haftmann and Christian Urban gave
-advice on Isabelle and package writing.
+Tobias Nipkow and Makarius Wenzel made this work possible. Andreas Lochbihler
+provided lots of comments on earlier versions of the package, especially for the
+coinductive part. Brian Huffman suggested major simplifications to the internal
+constructions, much of which has yet to be implemented. Florian Haftmann and
+Christian Urban provided general advice advice on Isabelle and package writing.
+Stefan Milius and Lutz Schr\"oder suggested an elegant prove to eliminate one of
+the BNF assumptions.
 *}
 
 end
diff -r e1c6fa322d96 -r 591e76f2651e src/Doc/manual.bib
--- a/src/Doc/manual.bib	Thu Aug 01 22:28:49 2013 +0200
+++ b/src/Doc/manual.bib	Thu Aug 01 22:37:04 2013 +0200
@@ -302,7 +302,7 @@
   crossref = {itp2010}}
 
 @unpublished{blanchette-et-al-wit,
-  author = {J.C. Blanchette and A. Popescu and D. Traytel},
+  author = {J. C. Blanchette and A. Popescu and D. Traytel},
   title = {Witnessing (Co)datatypes},
   year = 2013,
   note = {\url{http://www21.in.tum.de/~traytel/papers/witness/wit.pdf}}}