# HG changeset patch # User blanchet # Date 1408375213 -7200 # Node ID cbe9a16f8e1139cc72bab178531d6f459b6cd017 # Parent 6edc3529bb4e9d95e91ae201120429ba20383da0 added collection theorem for consistency and convenience diff -r 6edc3529bb4e -r cbe9a16f8e11 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Mon Aug 18 17:19:58 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Mon Aug 18 17:20:13 2014 +0200 @@ -831,6 +831,8 @@ \item[@{text "t."}\hthm{split_sel_asm}\rm:] ~ \\ @{thm list.split_sel_asm[no_vars]} +\item[@{text "t."}\hthm{split_sels} = @{text "split_sel split_sel_asm"}] + \item[@{text "t."}\hthm{case_eq_if}\rm:] ~ \\ @{thm list.case_eq_if[no_vars]} diff -r 6edc3529bb4e -r cbe9a16f8e11 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Aug 18 17:19:58 2014 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Aug 18 17:20:13 2014 +0200 @@ -216,6 +216,7 @@ val split_selN = "split_sel"; val split_sel_asmN = "split_sel_asm"; val splitsN = "splits"; +val split_selsN = "split_sels"; val case_cong_weak_thmsN = "case_cong_weak"; val cong_attrs = @{attributes [cong]}; @@ -987,7 +988,8 @@ (split_sel_asmN, split_sel_asm_thms, []), (splitN, [split_thm], []), (split_asmN, [split_asm_thm], []), - (splitsN, [split_thm, split_asm_thm], [])] + (splitsN, [split_thm, split_asm_thm], []), + (split_selsN, split_sel_thms @ split_sel_asm_thms, [])] |> filter_out (null o #2) |> map (fn (thmN, thms, attrs) => ((qualify true (Binding.name thmN), attrs), [(thms, [])]));