1.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Fri Jan 22 13:38:40 2010 +0100
     1.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Fri Jan 22 13:39:00 2010 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      UniqueFactorization.thy
     1.5 -    ID:         
     1.6      Author:     Jeremy Avigad
     1.7  
     1.8      
     1.9 @@ -388,7 +387,7 @@
    1.10    apply (subgoal_tac "multiset_prime_factorization n = Abs_multiset
    1.11        f")
    1.12    apply (unfold prime_factors_nat_def multiplicity_nat_def)
    1.13 -  apply (simp add: set_of_def count_def Abs_multiset_inverse multiset_def)
    1.14 +  apply (simp add: set_of_def Abs_multiset_inverse multiset_def)
    1.15    apply (unfold multiset_prime_factorization_def)
    1.16    apply (subgoal_tac "n > 0")
    1.17    prefer 2
    1.18 @@ -401,7 +400,7 @@
    1.19    apply force
    1.20    apply force
    1.21    apply force
    1.22 -  unfolding set_of_def count_def msetprod_def
    1.23 +  unfolding set_of_def msetprod_def
    1.24    apply (subgoal_tac "f : multiset")
    1.25    apply (auto simp only: Abs_multiset_inverse)
    1.26    unfolding multiset_def apply force