# HG changeset patch
# User desharna
# Date 1413296382 -7200
# Node ID 74a81d6f3c546b5338d1dd7dd337b2eb0894c5a1
# Parent  cdf84b6e1297dff5b7063e89580f7312a499c395
document 'sel_transfer'

diff -r cdf84b6e1297 -r 74a81d6f3c54 src/Doc/Datatypes/Datatypes.thy
--- 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]}