# HG changeset patch
# User blanchet
# Date 1427465311 -3600
# Node ID 057b1018d5893b0cf50e0a5e488c023b7edb1c9b
# Parent  a03696dc3283c1d142427740d222531f294420d2
clarified doc

diff -r a03696dc3283 -r 057b1018d589 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Mar 27 11:20:46 2015 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Mar 27 15:08:31 2015 +0100
@@ -865,25 +865,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}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
 
 \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}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
 
 \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}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
 
 \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}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
 
 \item[@{text "t."}\hthm{set} @{text "[simp, code]"}\rm:] ~ \\
 @{thm list.set(1)[no_vars]} \\
@@ -958,7 +958,7 @@
 \item[@{text "t."}\hthm{set_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
 @{thm list.set_transfer[no_vars]} \\
 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
 
 \item[@{text "t."}\hthm{map_cong0}\rm:] ~ \\
 @{thm list.map_cong0[no_vars]}
@@ -981,7 +981,7 @@
 \item[@{text "t."}\hthm{map_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
 @{thm list.map_transfer[no_vars]} \\
 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
 
 \item[@{text "t."}\hthm{rel_compp} @{text "[relator_distr]"}\rm:] ~ \\
 @{thm list.rel_compp[no_vars]} \\
@@ -1012,7 +1012,7 @@
 \item[@{text "t."}\hthm{rel_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
 @{thm list.rel_transfer[no_vars]} \\
 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
 
 \end{description}
 \end{indentblock}
@@ -1053,7 +1053,7 @@
 \item[@{text "t."}\hthm{rec_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
 @{thm list.rec_transfer[no_vars]} \\
 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
 
 \end{description}
 \end{indentblock}
@@ -1928,7 +1928,7 @@
 \item[@{text "t."}\hthm{corec_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
 @{thm llist.corec_transfer[no_vars]} \\
 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}).
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
 
 \end{description}
 \end{indentblock}
@@ -3066,7 +3066,8 @@
 the \hthm{transfer} plugin generates a predicator @{text "t.pred_t"} and
 properties that guide the Transfer tool.
 
-The plugin derives the following properties:
+For types with no dead type arguments (and at least one live type argument), the
+plugin derives the following properties:
 
 \begin{indentblock}
 \begin{description}