--- a/src/Doc/Datatypes/Datatypes.thy Tue Oct 14 16:17:36 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Tue Oct 14 16:19:42 2014 +0200
@@ -856,6 +856,10 @@
\item[@{text "t."}\hthm{case_transfer}\rm:] ~ \\
@{thm list.case_transfer[no_vars]}
+\item[@{text "t."}\hthm{sel_transfer}\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:] ~ \\
@{thm list.ctr_transfer(1)[no_vars]} \\
@{thm list.ctr_transfer(2)[no_vars]}