--- a/src/HOL/Number_Theory/UniqueFactorization.thy Wed Aug 19 22:09:33 2015 +0200
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy Wed Aug 19 22:40:41 2015 +0200
@@ -725,7 +725,7 @@
(is "_ = ?z")
proof -
have [arith]: "?z > 0"
- by (rule setprod_pos_nat) auto
+ by auto
have aux: "\<And>p. prime p \<Longrightarrow> multiplicity p ?z = min (multiplicity p x) (multiplicity p y)"
apply (subst multiplicity_prod_prime_powers_nat)
apply auto
@@ -759,7 +759,7 @@
(is "_ = ?z")
proof -
have [arith]: "?z > 0"
- by (rule setprod_pos_nat, auto)
+ by auto
have aux: "\<And>p. prime p \<Longrightarrow> multiplicity p ?z = max (multiplicity p x) (multiplicity p y)"
apply (subst multiplicity_prod_prime_powers_nat)
apply auto