# HG changeset patch
# User nipkow
# Date 1284446422 -7200
# Node ID aecb239a2bbc6ffd99e3f08eb131002d8627372a
# Parent  41ce0b56d85808b6363c7e7a0fc88bf797d0dadc
removed duplicate lemma

diff -r 41ce0b56d858 -r aecb239a2bbc src/HOL/Library/Multiset.thy
--- 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