# HG changeset patch
# User desharna
# Date 1400691334 -7200
# Node ID 90d4db566e122b790cd6b5ec110c4a8d505996f4
# Parent  b3613d7e108b98b6a655365e5a69418d74740efd
document property 'sel_map'

diff -r b3613d7e108b -r 90d4db566e12 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]}