# HG changeset patch
# User blanchet
# Date 1570718272 -7200
# Node ID 13d6b561b0ea4583cb2a2624dd68009e3054cbb3
# Parent  dd675800469d3e6294ce1f0daa94613268997613
added para constrasting 'primrec' and 'fun' -- and removed my middle name

diff -r dd675800469d -r 13d6b561b0ea src/Doc/Datatypes/Datatypes.thy
--- 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>
 
 
diff -r dd675800469d -r 13d6b561b0ea src/Doc/Datatypes/document/root.tex
--- 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}
 
diff -r dd675800469d -r 13d6b561b0ea src/Doc/Nitpick/document/root.tex
--- 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{}}
 
diff -r dd675800469d -r 13d6b561b0ea src/Doc/Sledgehammer/document/root.tex
--- 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 \\