--- a/src/HOL/Library/Multiset.thy Mon Sep 13 16:44:20 2010 +0200
+++ b/src/HOL/Library/Multiset.thy Tue Sep 14 08:40:22 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