# HG changeset patch
# User blanchet
# Date 1429465604 -7200
# Node ID ff997935a6544fdcf3aa0d53f13ab29668d1ca64
# Parent  4e1ba085be4acd2336fb2b3ad79ae01d9a1faf61
acknowledgment

diff -r 4e1ba085be4a -r ff997935a654 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Sun Apr 19 19:43:36 2015 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Sun Apr 19 19:46:44 2015 +0200
@@ -3228,11 +3228,12 @@
 versions of the package, especially on the coinductive part. Brian Huffman
 suggested major simplifications to the internal constructions. Ond\v{r}ej
 Kun\v{c}ar implemented the @{text transfer} and @{text lifting} plugins.
-Florian Haftmann and Christian Urban provided general advice on Isabelle and
-package writing. Stefan Milius and Lutz Schr\"oder found an elegant proof that
-eliminated one of the BNF proof obligations. Gerwin Klein, Andreas Lochbihler,
-Tobias Nipkow, and Christian Sternagel suggested many textual improvements to
-this tutorial.
+Christian Sternagel and Ren\'e Thiemann ported the \keyw{derive} command
+from the \emph{Archive of Formal Proofs} to the new datatypes. Florian Haftmann
+and Christian Urban provided general advice on Isabelle and package writing.
+Stefan Milius and Lutz Schr\"oder found an elegant proof that eliminated one of
+the BNF proof obligations. Gerwin Klein, Andreas Lochbihler, Tobias Nipkow, and
+Christian Sternagel suggested many textual improvements to this tutorial.
 *}
 
 end