# HG changeset patch
# User haftmann
# Date 1264163940 -3600
# Node ID e1b8f273640415617663d88ded5403cd6ca6d7dc
# Parent  aa5d27f1d9b914423768a123850c4b0db689a293
simplified proofs

diff -r aa5d27f1d9b9 -r e1b8f2736404 src/HOL/Number_Theory/UniqueFactorization.thy
--- 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