# 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