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

diff -r fd3b0135bc59 -r 74202654e4ee 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
@@ -2981,13 +2981,13 @@
   \label{ssec:code-generator} *}
 
 text {*
-The \hthm{code} plugin registers (co)datatypes and other freely generated types
-for code generation. No distinction is made between datatypes and codatatypes.
-This means that for target languages with a strict evaluation strategy (e.g.,
-Standard ML), programs that attempt to produce infinite codatatype values will
-not terminate.
-
-The plugin derives the following properties:
+The \hthm{code} plugin registers freely generated types, including
+(co)datatypes, and (co)recursive functions for code generation. No distinction
+is made between datatypes and codatatypes. This means that for target languages
+with a strict evaluation strategy (e.g., Standard ML), programs that attempt to
+produce infinite codatatype values will not terminate.
+
+For types, the plugin derives the following properties:
 
 \begin{indentblock}
 \begin{description}
@@ -3007,9 +3007,10 @@
 \end{indentblock}
 
 In addition, the plugin sets the @{text "[code]"} attribute on a number of
-properties of (co)datatypes and other freely generated types, as documented in
-Sections \ref{ssec:datatype-generated-theorems} and
-\ref{ssec:codatatype-generated-theorems}.
+properties of freely generated types and of (co)recursive functions, as
+documented in Sections \ref{ssec:datatype-generated-theorems},
+\ref{ssec:primrec-generated-theorems}, \ref{ssec:codatatype-generated-theorems},
+and~\ref{ssec:primcorec-generated-theorems}.
 *}