--- 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}
*}
--- 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