--- a/src/HOL/Number_Theory/UniqueFactorization.thy Wed Aug 15 14:00:12 2012 +0200
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy Wed Aug 15 14:26:42 2012 +0200
@@ -544,12 +544,7 @@
apply (erule ssubst)
apply (subst setprod_Un_disjoint)
apply auto
- apply (subgoal_tac "(\<Prod>p\<in>prime_factors l - prime_factors k. p ^ multiplicity p k) =
- (\<Prod>p\<in>prime_factors l - prime_factors k. 1)")
- apply (erule ssubst)
- apply (simp add: setprod_1)
- apply (erule prime_factorization_nat)
- apply (rule setprod_cong, auto)
+ apply(simp add: prime_factorization_nat)
apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors l Un
(prime_factors k - prime_factors l)")
apply (erule ssubst)
@@ -557,9 +552,7 @@
apply auto
apply (subgoal_tac "(\<Prod>p\<in>prime_factors k - prime_factors l. p ^ multiplicity p l) =
(\<Prod>p\<in>prime_factors k - prime_factors l. 1)")
- apply (erule ssubst)
- apply (simp add: setprod_1)
- apply (erule prime_factorization_nat)
+ apply (simp add: prime_factorization_nat)
apply (rule setprod_cong, auto)
done