src/HOL/Library/Multiset.thy
changeset 55913 c1409c103b77
parent 55811 aa1acc25126b
child 55945 e96383acecf9
     1.1 --- a/src/HOL/Library/Multiset.thy	Tue Mar 04 16:16:05 2014 -0800
     1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Mar 05 09:59:48 2014 +0100
     1.3 @@ -647,11 +647,10 @@
     1.4  lemma multi_nonempty_split: "M \<noteq> {#} \<Longrightarrow> \<exists>A a. M = A + {#a#}"
     1.5  by (induct M) auto
     1.6  
     1.7 -lemma multiset_cases [cases type, case_names empty add]:
     1.8 -assumes em:  "M = {#} \<Longrightarrow> P"
     1.9 -assumes add: "\<And>N x. M = N + {#x#} \<Longrightarrow> P"
    1.10 -shows "P"
    1.11 -using assms by (induct M) simp_all
    1.12 +lemma multiset_cases [cases type]:
    1.13 +  obtains (empty) "M = {#}"
    1.14 +    | (add) N x where "M = N + {#x#}"
    1.15 +  using assms by (induct M) simp_all
    1.16  
    1.17  lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
    1.18  by (cases "B = {#}") (auto dest: multi_member_split)