# HG changeset patch
# User desharna
# Date 1415359496 -3600
# Node ID 7d673ab6a8d9b859eee7aff6e0cabbbba1169a18
# Parent  0ef44616fd5fbb79c18cfa53b0ecd0d231523dd2
document '*_transfer' attribute

diff -r 0ef44616fd5f -r 7d673ab6a8d9 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Nov 07 11:52:56 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Nov 07 12:24:56 2014 +0100
@@ -853,20 +853,28 @@
 \begin{indentblock}
 \begin{description}
 
-\item[@{text "t."}\hthm{case_transfer}\rm:] ~ \\
-@{thm list.case_transfer[no_vars]}
-
-\item[@{text "t."}\hthm{sel_transfer}\rm:] ~ \\
+\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}.)
+
+\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.
-
-\item[@{text "t."}\hthm{ctr_transfer}\rm:] ~ \\
+selector to all constructors. \\
+(The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin,
+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]}
-
-\item[@{text "t."}\hthm{disc_transfer}\rm:] ~ \\
+@{thm list.ctr_transfer(2)[no_vars]} \\
+(The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin,
+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]}
+@{thm list.disc_transfer(2)[no_vars]} \\
+(The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin,
+Section~\ref{ssec:transfer}.)
 
 \item[@{text "t."}\hthm{set} @{text "[simp, code]"}\rm:] ~ \\
 @{thm list.set(1)[no_vars]} \\
@@ -938,8 +946,10 @@
 \item[@{text "t."}\hthm{set_map}\rm:] ~ \\
 @{thm list.set_map[no_vars]}
 
-\item[@{text "t."}\hthm{set_transfer}\rm:] ~ \\
-@{thm list.set_transfer[no_vars]}
+\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}.)
 
 \item[@{text "t."}\hthm{map_cong0}\rm:] ~ \\
 @{thm list.map_cong0[no_vars]}
@@ -959,8 +969,10 @@
 \item[@{text "t."}\hthm{map_ident}\rm:] ~ \\
 @{thm list.map_ident[no_vars]}
 
-\item[@{text "t."}\hthm{map_transfer}\rm:] ~ \\
-@{thm list.map_transfer[no_vars]}
+\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}.)
 
 \item[@{text "t."}\hthm{rel_compp} @{text "[relator_distr]"}\rm:] ~ \\
 @{thm list.rel_compp[no_vars]} \\
@@ -985,8 +997,10 @@
 (The @{text "[relator_mono]"} attribute is set by the @{text lifting} plugin,
 Section~\ref{ssec:lifting}.)
 
-\item[@{text "t."}\hthm{rel_transfer}\rm:] ~ \\
-@{thm list.rel_transfer[no_vars]}
+\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}.)
 
 \end{description}
 \end{indentblock}
@@ -1024,8 +1038,10 @@
 \item[@{text "t."}\hthm{rec_o_map}\rm:] ~ \\
 @{thm list.rec_o_map[no_vars]}
 
-\item[@{text "t."}\hthm{rec_transfer}\rm:] ~ \\
-@{thm list.rec_transfer[no_vars]}
+\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}.)
 
 \end{description}
 \end{indentblock}
@@ -1858,8 +1874,10 @@
 \item[@{text "t."}\hthm{map_o_corec}\rm:] ~ \\
 @{thm llist.map_o_corec[no_vars]}
 
-\item[@{text "t."}\hthm{corec_transfer}\rm:] ~ \\
-@{thm llist.corec_transfer[no_vars]}
+\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}.)
 
 \end{description}
 \end{indentblock}