added collection theorem for consistency and convenience
authorblanchet
Mon Aug 18 17:20:13 2014 +0200 (2014-08-18)
changeset 57984cbe9a16f8e11
parent 57983 6edc3529bb4e
child 57985 1e93e5265dc2
added collection theorem for consistency and convenience
src/Doc/Datatypes/Datatypes.thy
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Mon Aug 18 17:19:58 2014 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Mon Aug 18 17:20:13 2014 +0200
     1.3 @@ -831,6 +831,8 @@
     1.4  \item[@{text "t."}\hthm{split_sel_asm}\rm:] ~ \\
     1.5  @{thm list.split_sel_asm[no_vars]}
     1.6  
     1.7 +\item[@{text "t."}\hthm{split_sels} = @{text "split_sel split_sel_asm"}]
     1.8 +
     1.9  \item[@{text "t."}\hthm{case_eq_if}\rm:] ~ \\
    1.10  @{thm list.case_eq_if[no_vars]}
    1.11  
     2.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Aug 18 17:19:58 2014 +0200
     2.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Aug 18 17:20:13 2014 +0200
     2.3 @@ -216,6 +216,7 @@
     2.4  val split_selN = "split_sel";
     2.5  val split_sel_asmN = "split_sel_asm";
     2.6  val splitsN = "splits";
     2.7 +val split_selsN = "split_sels";
     2.8  val case_cong_weak_thmsN = "case_cong_weak";
     2.9  
    2.10  val cong_attrs = @{attributes [cong]};
    2.11 @@ -987,7 +988,8 @@
    2.12             (split_sel_asmN, split_sel_asm_thms, []),
    2.13             (splitN, [split_thm], []),
    2.14             (split_asmN, [split_asm_thm], []),
    2.15 -           (splitsN, [split_thm, split_asm_thm], [])]
    2.16 +           (splitsN, [split_thm, split_asm_thm], []),
    2.17 +           (split_selsN, split_sel_thms @ split_sel_asm_thms, [])]
    2.18            |> filter_out (null o #2)
    2.19            |> map (fn (thmN, thms, attrs) =>
    2.20              ((qualify true (Binding.name thmN), attrs), [(thms, [])]));