--- 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