
diff -r 1b4dc8a9f7d9 -r c5f6e2c4472c src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Jan 05 10:09:42 2015 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Jan 05 11:00:12 2015 +0100
@@ -124,9 +124,9 @@
 %\item Section \ref{sec:using-the-standard-ml-interface}, ``Using the Standard
 ML Interface,'' %describes the package's programmatic interface.
 
-\item Section \ref{sec:controlling-plugins}, ``Controlling Plugins,''
-is concerned with the package's interoperability with other Isabelle packages
-and tools, such as the code generator, Transfer, Lifting, and Quickcheck.
+\item Section \ref{sec:selecting-plugins}, ``Selecting Plugins,'' is concerned
+with the package's interoperability with other Isabelle packages and tools, such
+as the code generator, Transfer, Lifting, and Quickcheck.
 
 \item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and
 Limitations,'' concludes with known open issues at the time of writing.
@@ -184,7 +184,7 @@
 
 text {*
 \noindent
-Here, @{const Truue}, @{const Faalse}, and @{const Perhaaps} have the type @{typ trool}.
+@{const Truue}, @{const Faalse}, and @{const Perhaaps} have the type @{typ trool}.
 
 Polymorphic types are possible, such as the following option type, modeled after
 its homologue from the @{theory Option} theory:
@@ -198,8 +198,8 @@
 
 text {*
 \noindent
-The constructors are @{text "None :: 'a option"} and
-@{text "Some :: 'a \<Rightarrow> 'a option"}.
+The constructors are @{text "None \<Colon> 'a option"} and
+@{text "Some \<Colon> 'a \<Rightarrow> 'a option"}.
 
 The next example has three type parameters:
 *}
@@ -209,7 +209,7 @@
 text {*
 \noindent
 The constructor is
-@{text "Triple :: 'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> ('a, 'b, 'c) triple"}.
+@{text "Triple \<Colon> 'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> ('a, 'b, 'c) triple"}.
 Unlike in Standard ML, curried constructors are supported. The uncurried variant
 is also possible:
 *}
@@ -417,8 +417,8 @@
 
 The \keyw{where} clause at the end of the command specifies a default value for
 selectors applied to constructors on which they are not a priori specified.
-Here, it is used to ensure that the tail of the empty list is itself (instead of
-being left unspecified).
+In the example, it is used to ensure that the tail of the empty list is itself
+(instead of being left unspecified).
 
 Because @{const Nil} is nullary, it is also possible to use
 @{term "\<lambda>xs. xs = Nil"} as a discriminator. This is the default behavior
@@ -471,14 +471,15 @@
 \end{matharray}
 
 @{rail \<open>
-  @@{command datatype} target? @{syntax dt_options}? \<newline>
-    (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') \<newline>
-     @{syntax map_rel}? (@'where' (prop + '|'))? + @'and')
+  @@{command datatype} target? @{syntax dt_options}? @{syntax dt_spec}
   ;
   @{syntax_def dt_options}: '(' ((@{syntax plugins} | 'discs_sels') + ',') ')'
   ;
   @{syntax_def plugins}: 'plugins' ('only' | 'del') ':' (name +)
   ;
+  @{syntax_def dt_spec}: (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') \<newline>
+     @{syntax map_rel}? (@'where' (prop + '|'))? + @'and')
+  ;
   @{syntax_def map_rel}: @'for' ((('map' | 'rel') ':' name) +)
 \<close>}
 
@@ -653,7 +654,7 @@
 
 \noindent
 In addition, some of the plugins introduce their own constants
-(Section~\ref{sec:controlling-plugins}). The case combinator, discriminators,
+(Section~\ref{sec:selecting-plugins}). The case combinator, discriminators,
 and selectors are collectively called \emph{destructors}. The prefix
 ``@{text "t."}'' is an optional component of the names and is normally hidden.
 *}
@@ -686,7 +687,7 @@
 The full list of named theorems can be obtained as usual by entering the
 command \keyw{print_theorems} immediately after the datatype definition.
 This list includes theorems produced by plugins
-(Section~\ref{sec:controlling-plugins}), but normally excludes low-level
+(Section~\ref{sec:selecting-plugins}), but normally excludes low-level
 theorems that reveal internal constructions. To make these accessible, add
 the line
 *}
@@ -1104,7 +1105,7 @@
 @{const size} in terms of the generic function @{text "t.size_t"}.
 Moreover, the new function considers nested occurrences of a value, in the nested
 recursive case. The old behavior can be obtained by disabling the @{text size}
-plugin (Section~\ref{sec:controlling-plugins}) and instantiating the
+plugin (Section~\ref{sec:selecting-plugins}) and instantiating the
 @{text size} type class manually.
 
 \item \emph{The internal constructions are completely different.} Proof texts
@@ -1149,7 +1150,7 @@
 text {*
 Recursive functions over datatypes can be specified using the @{command primrec}
 command, which supports primitive recursion, or using the more general
-\keyw{fun} and \keyw{function} commands. Here, the focus is on
+\keyw{fun} and \keyw{function} commands. In this tutorial, the focus is on
 @{command primrec}; the other two commands are described in a separate
 tutorial @{cite "isabelle-function"}.
 
@@ -1489,7 +1490,7 @@
   @@{command primrec} target? @{syntax pr_options}? fixes \<newline>
   @'where' (@{syntax pr_equation} + '|')
   ;
-  @{syntax_def pr_options}: '(' (('nonexhaustive' | 'transfer') + ',') ')'
+  @{syntax_def pr_options}: '(' ((@{syntax plugins} | 'nonexhaustive' | 'transfer') + ',') ')'
   ;
   @{syntax_def pr_equation}: thmdecl? prop
 \<close>}
@@ -1512,12 +1513,16 @@
 \setlength{\itemsep}{0pt}
 
 \item
-The @{text "nonexhaustive"} option indicates that the functions are not
+The @{text plugins} option indicates which plugins should be enabled
+(@{text only}) or disabled (@{text del}). By default, all plugins are enabled.
+
+\item
+The @{text nonexhaustive} option indicates that the functions are not
 necessarily specified for all constructors. It can be used to suppress the
 warning that is normally emitted when some constructors are missing.
 
 \item
-The @{text "transfer"} option indicates that an unconditional transfer rule
+The @{text transfer} option indicates that an unconditional transfer rule
 should be generated and proved @{text "by transfer_prover"}. The
 @{text "[transfer_rule]"} attribute is set on the generated theorem.
 \end{itemize}
@@ -1754,8 +1759,7 @@
 \end{matharray}
 
 @{rail \<open>
-  @@{command codatatype} target? \<newline>
-    (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') + @'and')
+  @@{command codatatype} target? @{syntax dt_options}? @{syntax dt_spec}
 \<close>}
 
 \medskip
@@ -1912,9 +1916,9 @@
 text {*
 Corecursive functions can be specified using the @{command primcorec} and
 \keyw{prim\-corec\-ursive} commands, which support primitive corecursion, or
-using the more general \keyw{partial_function} command. Here, the focus is on
-the first two. More examples can be found in the directory
-\verb|~~/src/HOL/Datatype_Examples|.
+using the more general \keyw{partial_function} command. In this tutorial, the
+focus is on the first two. More examples can be found in the directory
+\verb|~~/src/HOL/Datatype_|\allowbreak\verb|Examples|.
 
 Whereas recursive functions consume datatypes one constructor at a time,
 corecursive functions construct codatatypes one constructor at a time.
@@ -2435,7 +2439,7 @@
   (@@{command primcorec} | @@{command primcorecursive}) target? \<newline>
     @{syntax pcr_options}? fixes @'where' (@{syntax pcr_formula} + '|')
   ;
-  @{syntax_def pcr_options}: '(' (('sequential' | 'exhaustive' | 'transfer') + ',') ')'
+  @{syntax_def pcr_options}: '(' ((@{syntax plugins} | 'sequential' | 'exhaustive' | 'transfer') + ',') ')'
   ;
   @{syntax_def pcr_formula}: thmdecl? prop (@'of' (term * ))?
 \<close>}
@@ -2458,16 +2462,20 @@
 \setlength{\itemsep}{0pt}
 
 \item
-The @{text "sequential"} option indicates that the conditions in specifications
+The @{text plugins} option indicates which plugins should be enabled
+(@{text only}) or disabled (@{text del}). By default, all plugins are enabled.
+
+\item
+The @{text sequential} option indicates that the conditions in specifications
 expressed using the constructor or destructor view are to be interpreted
 sequentially.
 
 \item
-The @{text "exhaustive"} option indicates that the conditions in specifications
+The @{text exhaustive} option indicates that the conditions in specifications
 expressed using the constructor or destructor view cover all possible cases.
 
 \item
-The @{text "transfer"} option indicates that an unconditional transfer rule
+The @{text transfer} option indicates that an unconditional transfer rule
 should be generated and proved @{text "by transfer_prover"}. The
 @{text "[transfer_rule]"} attribute is set on the generated theorem.
 \end{itemize}
@@ -2832,8 +2840,8 @@
 *)
 
 
-section {* Controlling Plugins
-  \label{sec:controlling-plugins} *}
+section {* Selecting Plugins
+  \label{sec:selecting-plugins} *}
 
 text {*
 Plugins extend the (co)datatype package to interoperate with other Isabelle
@@ -2964,6 +2972,10 @@
 
 \end{description}
 \end{indentblock}
+
+For @{command primrec}, @{command primcorec}, and @{command primcorecursive},
+the \hthm{transfer} plugin implements the generation of the @{text "f.transfer"}
+property, conditioned by the @{text transfer} option.
 *}
 
 
@@ -2998,7 +3010,7 @@
 
 text {*
 The integration of datatypes with Quickcheck is accomplished by the
-\hthm{quickcheck} plugin. It combines a number of subplugins that instantiate
+\hthm{quick\-check} plugin. It combines a number of subplugins that instantiate
 specific type classes. The subplugins can be enabled or disabled individually.
 They are listed below:
 




