diff -r 37c31a619eee -r bf74357f91f8 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Thu Sep 26 13:42:13 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Sep 26 13:42:14 2013 +0200
@@ -787,6 +787,12 @@
 \item[@{text "t."}\hthm{expand}\rm:] ~ \\
 @{thm list.expand[no_vars]}
 
+\item[@{text "t."}\hthm{sel\_split}\rm:] ~ \\
+@{thm list.sel_split[no_vars]}
+
+\item[@{text "t."}\hthm{sel\_split\_asm}\rm:] ~ \\
+@{thm list.sel_split_asm[no_vars]}
+
 \item[@{text "t."}\hthm{case\_conv\_if}\rm:] ~ \\
 @{thm list.case_conv_if[no_vars]}