--- a/src/Doc/Datatypes/Datatypes.thy Thu Oct 10 16:59:37 2019 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Fri Oct 11 11:08:32 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}
@@ -1738,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}
@@ -2026,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>