document property 'sel_map'
authordesharna
Wed, 21 May 2014 18:55:34 +0200
changeset 57047 90d4db566e12
parent 57046 b3613d7e108b
child 57050 362c8c64ec83
document property 'sel_map'
src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed May 21 18:55:34 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed May 21 18:55:34 2014 +0200
@@ -863,6 +863,9 @@
 \item[@{text "t."}\hthm{disc\_map\_iff} @{text "[simp]"}\rm:] ~ \\
 @{thm list.disc_map_iff[no_vars]}
 
+\item[@{text "t."}\hthm{sel\_map}\rm:] ~ \\
+@{thm list.sel_map[no_vars]}
+
 \item[@{text "t."}\hthm{rel\_inject} @{text "[simp]"}\rm:] ~ \\
 @{thm list.rel_inject(1)[no_vars]} \\
 @{thm list.rel_inject(2)[no_vars]}