--- a/src/Doc/Datatypes/Datatypes.thy Wed Oct 09 14:51:54 2019 +0000
+++ b/src/Doc/Datatypes/Datatypes.thy Thu Oct 10 16:37:52 2019 +0200
@@ -1227,10 +1227,17 @@
text \<open>
Recursive functions over datatypes can be specified using the @{command primrec}
-command, which supports primitive recursion, or using the more general
-\keyw{fun}, \keyw{function}, and \keyw{partial_function} commands. In this
-tutorial, the focus is on @{command primrec}; \keyw{fun} and \keyw{function} are
-described in a separate tutorial @{cite "isabelle-function"}.
+command, which supports primitive recursion, or using the \keyw{fun},
+\keyw{function}, and \keyw{partial_function} commands. In this tutorial, the
+focus is on @{command primrec}; \keyw{fun} and \keyw{function} are described in
+a separate tutorial @{cite "isabelle-function"}.
+
+Because it is restricted to primitive recursion, @{command primrec} is less
+powerful than \keyw{fun} and \keyw{function}. However, there are primitively
+recursive specifications (e.g., based on infinitely branching or mutually
+recursive datatypes) for which \keyw{fun}'s termination check fails. It is also
+good style to use the simpler @{command primrec} mechanism when it works, both
+as an optimization and as documentation.
\<close>
--- a/src/Doc/Datatypes/document/root.tex Wed Oct 09 14:51:54 2019 +0000
+++ b/src/Doc/Datatypes/document/root.tex Thu Oct 10 16:37:52 2019 +0200
@@ -59,7 +59,7 @@
\title{%\includegraphics[scale=0.5]{isabelle_hol} \\[4ex]
Defining (Co)datatypes and Primitively (Co)recursive Functions in Isabelle/HOL}
-\author{Julian Biendarra, Jasmin Christian Blanchette, \\
+\author{Julian Biendarra, Jasmin Blanchette, \\
Martin Desharnais, Lorenz Panny, \\
Andrei Popescu, and Dmitriy Traytel}
--- a/src/Doc/Nitpick/document/root.tex Wed Oct 09 14:51:54 2019 +0000
+++ b/src/Doc/Nitpick/document/root.tex Thu Oct 10 16:37:52 2019 +0200
@@ -54,7 +54,7 @@
Picking Nits \\[\smallskipamount]
\Large A User's Guide to Nitpick for Isabelle/HOL}
\author{\hbox{} \\
-Jasmin Christian Blanchette \\
+Jasmin Blanchette \\
{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\
\hbox{}}
--- a/src/Doc/Sledgehammer/document/root.tex Wed Oct 09 14:51:54 2019 +0000
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Oct 10 16:37:52 2019 +0200
@@ -58,7 +58,7 @@
Hammering Away \\[\smallskipamount]
\Large A User's Guide to Sledgehammer for Isabelle/HOL}
\author{\hbox{} \\
-Jasmin Christian Blanchette \\
+Jasmin Blanchette \\
{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\[4\smallskipamount]
{\normalsize with contributions from} \\[4\smallskipamount]
Lawrence C. Paulson \\