1.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Wed May 12 22:33:10 2010 -0700
     1.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Thu May 13 14:34:05 2010 +0200
     1.3 @@ -56,11 +56,6 @@
     1.4    apply auto
     1.5  done
     1.6   
     1.7 -(* Should this go in Multiset.thy? *)
     1.8 -(* TN: No longer an intro-rule; needed only once and might get in the way *)
     1.9 -lemma multiset_eqI: "[| !!x. count M x = count N x |] ==> M = N"
    1.10 -  by (subst multiset_eq_conv_count_eq, blast)
    1.11 -
    1.12  (* Here is a version of set product for multisets. Is it worth moving
    1.13     to multiset.thy? If so, one should similarly define msetsum for abelian 
    1.14     semirings, using of_nat. Also, is it worth developing bounded quantifiers 
    1.15 @@ -210,7 +205,7 @@
    1.16      ultimately have "count M a = count N a"
    1.17        by auto
    1.18    }
    1.19 -  thus ?thesis by (simp add:multiset_eq_conv_count_eq)
    1.20 +  thus ?thesis by (simp add:multiset_ext_iff)
    1.21  qed
    1.22  
    1.23  definition multiset_prime_factorization :: "nat => nat multiset" where