# HG changeset patch
# User blanchet
# Date 1444204978 -7200
# Node ID 24e7b6c915147d01a2cd63a9c0aceefed252c41b
# Parent  d7215449be83ee8d53e8f693b288bd80e78196a7
made documentation more accurate

diff -r d7215449be83 -r 24e7b6c91514 src/Doc/Datatypes/Datatypes.thy
--- 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}.