src/HOL/Number_Theory/UniqueFactorization.thy
changeset 39302 d7728f65b353
parent 37290 3464d7232670
child 40461 e876e95588ce
     1.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Mon Sep 13 11:13:15 2010 +0200
     1.3 @@ -213,7 +213,7 @@
     1.4      ultimately have "count M a = count N a"
     1.5        by auto
     1.6    }
     1.7 -  thus ?thesis by (simp add:multiset_ext_iff)
     1.8 +  thus ?thesis by (simp add:multiset_eq_iff)
     1.9  qed
    1.10  
    1.11  definition multiset_prime_factorization :: "nat => nat multiset" where