--- a/src/Doc/Datatypes/Datatypes.thy Fri Oct 11 22:01:45 2019 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Fri Oct 11 22:06:49 2019 +0200
@@ -1151,13 +1151,33 @@
by countable_datatype
+subsection \<open>Antiquotation
+ \label{ssec:datatype-antiquotation}\<close>
+
+subsubsection \<open>\textit{datatype}
+ \label{sssec:datatype-datatype}\<close>
+
+text \<open>
+The \textit{datatype} antiquotation, written
+\texttt{\char`\\\char`<\char`^}\verb|datatype>|\guilsinglleft\textit{t}\guilsinglright{}
+or \texttt{@}\verb|{datatype| \textit{t}\verb|}|, where \textit{t} is a type
+name, expands to \LaTeX{} code for the definition of the datatype, with each
+constructor listed with its argument types. For example, if \textit{t} is
+@{type option}:
+
+\begin{quote}
+\<^datatype>\<open>option\<close>
+\end{quote}
+\<close>
+
+
subsection \<open>Compatibility Issues
\label{ssec:datatype-compatibility-issues}\<close>
text \<open>
The command @{command datatype} has been designed to be highly compatible with
-the old command, to ease migration. There are nonetheless a few
-incompatibilities that may arise when porting:
+the old, pre-Isabelle2015 command, to ease migration. There are nonetheless a
+few incompatibilities that may arise when porting:
\begin{itemize}
\setlength{\itemsep}{0pt}
@@ -1227,10 +1247,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>
@@ -1731,9 +1758,9 @@
text \<open>
The command @{command primrec}'s behavior on new-style datatypes has been
-designed to be highly compatible with that for old-style datatypes, to ease
-migration. There is nonetheless at least one incompatibility that may arise when
-porting to the new package:
+designed to be highly compatible with that for old, pre-Isabelle2015 datatypes,
+to ease migration. There is nonetheless at least one incompatibility that may
+arise when porting to the new package:
\begin{itemize}
\setlength{\itemsep}{0pt}
@@ -2019,6 +2046,26 @@
\<close>
+subsection \<open>Antiquotation
+ \label{ssec:codatatype-antiquotation}\<close>
+
+subsubsection \<open>\textit{codatatype}
+ \label{sssec:codatatype-codatatype}\<close>
+
+text \<open>
+The \textit{codatatype} antiquotation, written
+\texttt{\char`\\\char`<\char`^}\verb|codatatype>|\guilsinglleft\textit{t}\guilsinglright{}
+or \texttt{@}\verb|{codatatype| \textit{t}\verb|}|, where \textit{t} is a type
+name, expands to \LaTeX{} code for the definition of the codatatype, with each
+constructor listed with its argument types. For example, if \textit{t} is
+@{type llist}:
+
+\begin{quote}
+\<^codatatype>\<open>llist\<close>
+\end{quote}
+\<close>
+
+
section \<open>Defining Primitively Corecursive Functions
\label{sec:defining-primitively-corecursive-functions}\<close>
--- a/src/Doc/Datatypes/document/root.tex Fri Oct 11 22:01:45 2019 +0200
+++ b/src/Doc/Datatypes/document/root.tex Fri Oct 11 22:06:49 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 Fri Oct 11 22:01:45 2019 +0200
+++ b/src/Doc/Nitpick/document/root.tex Fri Oct 11 22:06:49 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 Fri Oct 11 22:01:45 2019 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Fri Oct 11 22:06:49 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 \\
@@ -158,10 +158,10 @@
\begin{sloppy}
\begin{enum}
\item[\labelitemi] If you installed an official Isabelle package, it should
-already include properly setup executables for CVC4, E, SPASS, Vampire, veriT,
-and Z3, ready to use. To use Vampire, you must confirm that you are a
-noncommercial user, as indicated by the message that is displayed when
-Sledgehammer is invoked the first time.
+already include properly setup executables for CVC4, E, SPASS, Vampire, and Z3,
+ready to use. To use Vampire, you must confirm that you are a noncommercial
+user, as indicated by the message that is displayed when Sledgehammer is
+invoked the first time.
\item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3,
CVC4, E, SPASS, Vampire, and Z3 binary packages from \download. Extract the
@@ -200,7 +200,7 @@
variable \texttt{CVC3\_\allowbreak SOLVER}, \texttt{CVC4\_\allowbreak SOLVER},
\texttt{VERIT\_\allowbreak SOLVER}, or \texttt{Z3\_SOLVER} to the complete path
of the executable, \emph{including the file name}. Sledgehammer has been tested
-with CVC3 2.2 and 2.4.1, CVC4 1.5-prerelease, veriT smtcomp2014, and Z3 4.3.2.
+with CVC3 2.2 and 2.4.1, CVC4 1.5-prerelease, veriT smtcomp2019, and Z3 4.3.2.
Since Z3's output format is somewhat unstable, other versions of the solver
might not work well with Sledgehammer. Ideally, also set
\texttt{CVC3\_VERSION}, \texttt{CVC4\_VERSION}, \texttt{VERIT\_VERSION}, or
@@ -833,7 +833,7 @@
It is specifically designed to produce detailed proofs for reconstruction in
proof assistants. To use veriT, set the environment variable
\texttt{VERIT\_SOLVER} to the complete path of the executable, including the
-file name. Sledgehammer has been tested with version smtcomp2014.
+file name. Sledgehammer has been tested with version smtcomp2019.
\item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
Microsoft Research \cite{z3}. To use Z3, set the environment variable