# HG changeset patch
# User blanchet
# Date 1429726020 -7200
# Node ID bcb680bbcd0009166dd11a26422f7b2bc9c2f603
# Parent  123ac30760df44106f5c786dd7ad7268733554bb
improved docs

diff -r 123ac30760df -r bcb680bbcd00 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Apr 22 13:48:34 2015 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Apr 22 20:07:00 2015 +0200
@@ -86,8 +86,8 @@
 internal constructions and most of the internal proof obligations are omitted
 if the @{text quick_and_dirty} option is enabled.}
 The package is described in a number of papers
-@{cite "traytel-et-al-2012" and "blanchette-et-al-wit" and
-  "blanchette-et-al-2014-impl" and "panny-et-al-2014"}.
+@{cite "traytel-et-al-2012" and "blanchette-et-al-2014-impl" and
+"panny-et-al-2014" and "blanchette-et-al-2015-wit"}.
 The central notion is that of a \emph{bounded natural functor} (BNF)---a
 well-behaved type constructor for which nested (co)recursion is supported.
 
@@ -140,18 +140,10 @@
 
 \newcommand\authoremaili{\texttt{blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak
 in.\allowbreak tum.\allowbreak de}}
-\newcommand\authoremailii{\texttt{desh{\color{white}NOSPAM}\kern-\wd\boxA{}arna@\allowbreak
-in.\allowbreak tum.\allowbreak de}}
-\newcommand\authoremailiii{\texttt{lore{\color{white}NOSPAM}\kern-\wd\boxA{}nz.panny@\allowbreak
-in.\allowbreak tum.\allowbreak de}}
-\newcommand\authoremailiv{\texttt{pope{\color{white}NOSPAM}\kern-\wd\boxA{}scua@\allowbreak
-in.\allowbreak tum.\allowbreak de}}
-\newcommand\authoremailv{\texttt{tray{\color{white}NOSPAM}\kern-\wd\boxA{}tel@\allowbreak
-in.\allowbreak tum.\allowbreak de}}
 
 Comments and bug reports concerning either the package or this tutorial should
-be directed to the authors at \authoremaili, \authoremailii, \authoremailiii,
-\authoremailiv, and \authoremailv.
+be directed to the first author at \authoremaili or to the
+\texttt{cl-isabelle-users} mailing list.
 *}
 
 
@@ -2651,7 +2643,7 @@
 text {*
 Bounded natural functors (BNFs) are a semantic criterion for where
 (co)re\-cur\-sion may appear on the right-hand side of an equation
-@{cite "traytel-et-al-2012" and "blanchette-et-al-wit"}.
+@{cite "traytel-et-al-2012" and "blanchette-et-al-2015-wit"}.
 
 An $n$-ary BNF is a type constructor equipped with a map function
 (functorial action), $n$ set functions (natural transformations),
@@ -3216,6 +3208,10 @@
 \emph{The names of variables are often suboptimal in the properties generated by
 the package.}
 
+\item
+\emph{The compatibility layer sometimes produces induction principles with a
+slightly different shape than the old package.}
+
 \end{enumerate}
 *}
 
diff -r 123ac30760df -r bcb680bbcd00 src/Doc/manual.bib
--- a/src/Doc/manual.bib	Wed Apr 22 13:48:34 2015 +0200
+++ b/src/Doc/manual.bib	Wed Apr 22 20:07:00 2015 +0200
@@ -332,11 +332,19 @@
   author = "Jasmin Christian Blanchette and Tobias Nipkow",
   crossref = {itp2010}}
 
-@unpublished{blanchette-et-al-wit,
-  author = {J. C. Blanchette and A. Popescu and D. Traytel},
-  title = {Witnessing (Co)datatypes},
-  year = 2014,
-  note = {\url{http://www21.in.tum.de/~blanchet/wit.pdf}}}
+@inproceedings{blanchette-et-al-2015-wit,
+  author    = {Jasmin Christian Blanchette and
+               Andrei Popescu and
+               Dmitriy Traytel},
+  title     = {Witnessing (Co)datatypes},
+  booktitle = {{ESOP} 2015},
+  pages     = {359--382},
+  year      = {2015},
+  editor    = {Jan Vitek},
+  series    = {LNCS},
+  volume    = {9032},
+  publisher = {Springer}
+}
 
 @inproceedings{blanchette-et-al-2014-impl,
   author = "Jasmin Christian Blanchette and Johannes H{\"o}lzl