# HG changeset patch
# User blanchet
# Date 1425399651 -3600
# Node ID d8fff0b94c53ea0db5f97025af5a2a9b99b791c2
# Parent  5f56d4ff6635f3f1c7fb25ef06340712103b1c47
updated docs

diff -r 5f56d4ff6635 -r d8fff0b94c53 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Tue Mar 03 16:37:45 2015 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Mar 03 17:20:51 2015 +0100
@@ -3069,7 +3069,8 @@
 
 \item[@{text "t."}\hthm{pred_inject} @{text "[simp]"}\rm:] ~ \\
 @{thm list.pred_inject(1)[no_vars]} \\
-@{thm list.pred_inject(2)[no_vars]}
+@{thm list.pred_inject(2)[no_vars]} \\
+This property is generated only for (co)datatypes.
 
 \item[@{text "t."}\hthm{rel_eq_onp}\rm:] ~ \\
 @{thm list.rel_eq_onp[no_vars]}
@@ -3095,9 +3096,18 @@
 \end{description}
 \end{indentblock}
 
+\begin{sloppy}
+In addition, 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}
+
 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.
+the plugin implements the generation of the @{text "f.transfer"} property,
+conditioned by the @{text transfer} option, and sets the
+@{text "[transfer_rule]"} attribute on these.
 *}