src/Doc/Datatypes/Datatypes.thy
changeset 57047 90d4db566e12
parent 56995 61855ade6c7e
child 57079 aa7f051ba6ab
--- 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]}