src/HOL/Number_Theory/UniqueFactorization.thy
changeset 34947 e1b8f2736404
parent 33657 a4179bf442d1
child 35054 a5db9779b026
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Fri Jan 22 13:38:40 2010 +0100
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Fri Jan 22 13:39:00 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      UniqueFactorization.thy
-    ID:         
     Author:     Jeremy Avigad
 
     
@@ -388,7 +387,7 @@
   apply (subgoal_tac "multiset_prime_factorization n = Abs_multiset
       f")
   apply (unfold prime_factors_nat_def multiplicity_nat_def)
-  apply (simp add: set_of_def count_def Abs_multiset_inverse multiset_def)
+  apply (simp add: set_of_def Abs_multiset_inverse multiset_def)
   apply (unfold multiset_prime_factorization_def)
   apply (subgoal_tac "n > 0")
   prefer 2
@@ -401,7 +400,7 @@
   apply force
   apply force
   apply force
-  unfolding set_of_def count_def msetprod_def
+  unfolding set_of_def msetprod_def
   apply (subgoal_tac "f : multiset")
   apply (auto simp only: Abs_multiset_inverse)
   unfolding multiset_def apply force