src/Doc/Datatypes/Datatypes.thy
changeset 58677 74a81d6f3c54
parent 58659 6c9821c32dd5
child 58733 797d0e7aefc7
--- 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]}