removed problematic simp rule
authoreberlm <eberlm@in.tum.de>
Mon Apr 03 22:18:56 2017 +0200 (2017-04-03)
changeset 653544ff2ba82d668
parent 65353 ac9391e04ef2
child 65364 db7c97cdcfe7
child 65395 7504569a73c7
removed problematic simp rule
src/HOL/Library/Multiset.thy
     1.1 --- a/src/HOL/Library/Multiset.thy	Mon Apr 03 19:41:17 2017 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Mon Apr 03 22:18:56 2017 +0200
     1.3 @@ -1894,7 +1894,7 @@
     1.4    ultimately show ?case by simp
     1.5  qed
     1.6  
     1.7 -lemma mset_shuffle [simp]: "zs \<in> shuffle xs ys \<Longrightarrow> mset zs = mset xs + mset ys"
     1.8 +lemma mset_shuffle: "zs \<in> shuffle xs ys \<Longrightarrow> mset zs = mset xs + mset ys"
     1.9    by (induction xs ys arbitrary: zs rule: shuffle.induct) auto
    1.10  
    1.11  lemma mset_insort [simp]: "mset (insort x xs) = add_mset x (mset xs)"