--- a/src/Doc/Datatypes/Datatypes.thy Wed Oct 07 10:02:43 2015 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Wed Oct 07 10:02:58 2015 +0200
@@ -849,9 +849,11 @@
\label{sssec:functorial-theorems} *}
text {*
-The functorial theorems are partitioned in two subgroups. The first subgroup
-consists of properties involving the constructors or the destructors and either
-a set function, the map function, or the relator:
+The functorial theorems are generated for type constructors with at least
+one live type argument (e.g., @{typ "'a list"}). They are partitioned in two
+subgroups. The first subgroup consists of properties involving the
+constructors or the destructors and either a set function, the map function,
+or the relator:
\begin{indentblock}
\begin{description}
@@ -859,25 +861,25 @@
\item[@{text "t."}\hthm{case_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
@{thm list.case_transfer[no_vars]} \\
The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
+(Section~\ref{ssec:transfer}).
\item[@{text "t."}\hthm{sel_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
This property is missing for @{typ "'a list"} because there is no common
selector to all constructors. \\
The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
+(Section~\ref{ssec:transfer}).
\item[@{text "t."}\hthm{ctr_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
@{thm list.ctr_transfer(1)[no_vars]} \\
@{thm list.ctr_transfer(2)[no_vars]} \\
The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
+(Section~\ref{ssec:transfer}) .
\item[@{text "t."}\hthm{disc_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
@{thm list.disc_transfer(1)[no_vars]} \\
@{thm list.disc_transfer(2)[no_vars]} \\
The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
+(Section~\ref{ssec:transfer}).
\item[@{text "t."}\hthm{set} @{text "[simp, code]"}\rm:] ~ \\
@{thm list.set(1)[no_vars]} \\
@@ -3210,8 +3212,8 @@
the \hthm{transfer} plugin generates a predicator @{text "t.pred_t"} and
properties that guide the Transfer tool.
-For types with no dead type arguments (and at least one live type argument), the
-plugin derives the following properties:
+For types with at least one live type argument and \emph{no dead type
+arguments}, the plugin derives the following properties:
\begin{indentblock}
\begin{description}
@@ -3248,13 +3250,14 @@
\end{description}
\end{indentblock}
-\begin{sloppy}
-In addition, the plugin sets the @{text "[transfer_rule]"} attribute on the
-following (co)datatypes properties:
+For (co)datatypes with at least one live type argument, the plugin sets the
+@{text "[transfer_rule]"} attribute on the following (co)datatypes properties:
@{text "t.case_transfer"}, @{text "t.sel_transfer"}, @{text "t.ctr_transfer"},
-@{text "t.disc_transfer"}, @{text "t.set_transfer"}, @{text "t.map_transfer"},
-@{text "t.rel_transfer"}, @{text "t.rec_transfer"}, and @{text "t.corec_transfer"}.
-\end{sloppy}
+@{text "t.disc_transfer"}, @{text "t.rec_transfer"}, and @{text
+"t.corec_transfer"}. For (co)datatypes that further have \emph{no dead type
+arguments}, the plugin sets @{text "[transfer_rule]"} on
+@{text "t.set_transfer"}, @{text "t.map_transfer"}, and
+@{text "t.rel_transfer"}.
For @{command primrec}, @{command primcorec}, and @{command primcorecursive},
the plugin implements the generation of the @{text "f.transfer"} property,
@@ -3268,8 +3271,8 @@
text {*
For each (co)datatype and each manually registered BNF with at least one live
-type argument and no dead type arguments, the \hthm{lifting} plugin generates
-properties and attributes that guide the Lifting tool.
+type argument \emph{and no dead type arguments}, the \hthm{lifting} plugin
+generates properties and attributes that guide the Lifting tool.
The plugin derives the following property:
@@ -3282,7 +3285,7 @@
\end{description}
\end{indentblock}
-In addition, the plugin sets the @{text "[relator_eq_onp]"} attribute on a
+In addition, the plugin sets the @{text "[relator_eq]"} attribute on a
variant of the @{text t.rel_eq_onp} property generated by the @{text lifting}
plugin, the @{text "[relator_mono]"} attribute on @{text t.rel_mono}, and the
@{text "[relator_distr]"} attribute on @{text t.rel_compp}.