# HG changeset patch
# User blanchet
# Date 1570784912 -7200
# Node ID 77c8b8e73f883e46182b3e0da59601f63c99271a
# Parent  ed89f20de7abb9e7b20bf87d6b0f832e2528f5ad
document antiquotations + clarify porting text slightly

diff -r ed89f20de7ab -r 77c8b8e73f88 src/Doc/Datatypes/Datatypes.thy
--- 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>