docs
authorblanchet
Tue Jan 06 09:59:43 2015 +0100 (2015-01-06)
changeset 5929974202654e4ee
parent 59298 fd3b0135bc59
child 59300 7009e5fa5cd3
docs
src/Doc/Datatypes/Datatypes.thy
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Tue Jan 06 09:59:43 2015 +0100
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Tue Jan 06 09:59:43 2015 +0100
     1.3 @@ -2981,13 +2981,13 @@
     1.4    \label{ssec:code-generator} *}
     1.5  
     1.6  text {*
     1.7 -The \hthm{code} plugin registers (co)datatypes and other freely generated types
     1.8 -for code generation. No distinction is made between datatypes and codatatypes.
     1.9 -This means that for target languages with a strict evaluation strategy (e.g.,
    1.10 -Standard ML), programs that attempt to produce infinite codatatype values will
    1.11 -not terminate.
    1.12 -
    1.13 -The plugin derives the following properties:
    1.14 +The \hthm{code} plugin registers freely generated types, including
    1.15 +(co)datatypes, and (co)recursive functions for code generation. No distinction
    1.16 +is made between datatypes and codatatypes. This means that for target languages
    1.17 +with a strict evaluation strategy (e.g., Standard ML), programs that attempt to
    1.18 +produce infinite codatatype values will not terminate.
    1.19 +
    1.20 +For types, the plugin derives the following properties:
    1.21  
    1.22  \begin{indentblock}
    1.23  \begin{description}
    1.24 @@ -3007,9 +3007,10 @@
    1.25  \end{indentblock}
    1.26  
    1.27  In addition, the plugin sets the @{text "[code]"} attribute on a number of
    1.28 -properties of (co)datatypes and other freely generated types, as documented in
    1.29 -Sections \ref{ssec:datatype-generated-theorems} and
    1.30 -\ref{ssec:codatatype-generated-theorems}.
    1.31 +properties of freely generated types and of (co)recursive functions, as
    1.32 +documented in Sections \ref{ssec:datatype-generated-theorems},
    1.33 +\ref{ssec:primrec-generated-theorems}, \ref{ssec:codatatype-generated-theorems},
    1.34 +and~\ref{ssec:primcorec-generated-theorems}.
    1.35  *}
    1.36  
    1.37