# HG changeset patch
# User blanchet
# Date 1420534783 -3600
# Node ID 7009e5fa5cd350bee76d7f56f9fe9d06bdd37441
# Parent  74202654e4ee71a86d87864398c9716c51d46142
docs

diff -r 74202654e4ee -r 7009e5fa5cd3 src/Doc/Datatypes/Datatypes.thy
--- 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
diff -r 74202654e4ee -r 7009e5fa5cd3 src/Doc/Datatypes/document/root.tex
--- 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