--- a/src/Doc/Datatypes/Datatypes.thy Tue Jan 06 09:59:43 2015 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Tue Jan 06 09:59:43 2015 +0100
@@ -2969,9 +2969,9 @@
packages and tools, such as the code generator, Transfer, Lifting, and
Quickcheck. They can be enabled or disabled individually using the
@{syntax plugins} option to the commands @{command datatype},
-@{command codatatype}, @{command free_constructors}, @{command bnf}, and
-@{command bnf_axiomatization}.
-For example:
+@{command primrec}, @{command codatatype}, @{command primcorec},
+@{command primcorecursive}, @{command bnf}, @{command bnf_axiomatization}, and
+@{command free_constructors}. For example:
*}
datatype (plugins del: code "quickcheck") color = Red | Black
--- a/src/Doc/Datatypes/document/root.tex Tue Jan 06 09:59:43 2015 +0100
+++ b/src/Doc/Datatypes/document/root.tex Tue Jan 06 09:59:43 2015 +0100
@@ -58,7 +58,7 @@
\isadroptag{theory}
\title{%\includegraphics[scale=0.5]{isabelle_hol} \\[4ex]
-Defining (Co)datatypes in Isabelle/HOL}
+Defining (Co)datatypes and Primitively (Co)recursive Functions in Isabelle/HOL}
\author{Jasmin Christian Blanchette,
Martin Desharnais, \\
Lorenz Panny,
@@ -71,12 +71,17 @@
\maketitle
+\begin{sloppy}
\begin{abstract}
\noindent
-This tutorial describes the definitional package for datatypes and codatatypes
-in Isabelle/HOL. The package provides four main commands: \keyw{datatype},
-\keyw{codatatype}, \keyw{primrec}, and \keyw{primcorec}.
+This tutorial describes the definitional package for datatypes and codatatypes,
+and for primitively recursive and corecursive functions, in Isabelle/HOL. The
+package provides these commands:
+\keyw{datatype}, \keyw{datatype_compat}, \keyw{primrec}, \keyw{codatatype},
+\keyw{primcorec}, \keyw{prim\-co\-recursive}, \keyw{bnf}, \keyw{bnf_axiomatization},
+\keyw{print_bnfs}, and \keyw{free_\allowbreak constructors}.
\end{abstract}
+\end{sloppy}
\tableofcontents