# HG changeset patch
# User blanchet
# Date 1444207333 -7200
# Node ID 821ba62ed31b56898be20f99ac6bbbd0f6815590
# Parent  24e7b6c915147d01a2cd63a9c0aceefed252c41b
updated docs

diff -r 24e7b6c91514 -r 821ba62ed31b src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Oct 07 10:02:58 2015 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Oct 07 10:42:13 2015 +0200
@@ -860,8 +860,10 @@
 
 \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
+This property is generated by the @{text transfer} plugin
 (Section~\ref{ssec:transfer}).
+%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