| changeset 53917 | bf74357f91f8 |
| parent 53916 | 37c31a619eee |
| child 53997 | 8ff43f638da2 |
--- 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]}