# HG changeset patch
# User blanchet
# Date 1284447046 -7200
# Node ID cd20519eb9d027267f9afac2c2e38978d4e415cd
# Parent  aecb239a2bbc6ffd99e3f08eb131002d8627372a# Parent  7f11d833d65b0e5976eeda434dc9345e4b684bd6
merged

diff -r 7f11d833d65b -r cd20519eb9d0 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Sep 13 21:24:10 2010 +0200
+++ b/src/HOL/Library/Multiset.thy	Tue Sep 14 08:50:46 2010 +0200
@@ -1381,14 +1381,6 @@
 
 lemma fold_mset_insert:
   "fold_mset f z (A + {#x#}) = f x (fold_mset f z A)"
-apply (simp add: fold_mset_def fold_mset_insert_aux add_commute)  
-apply (rule the_equality)
- apply (auto cong add: conj_cong 
-     simp add: fold_mset_def [symmetric] fold_mset_equality fold_msetG_nonempty)
-done
-
-lemma fold_mset_insert_idem:
-  "fold_mset f z (A + {#a#}) = f a (fold_mset f z A)"
 apply (simp add: fold_mset_def fold_mset_insert_aux)
 apply (rule the_equality)
  apply (auto cong add: conj_cong