# HG changeset patch
# User wenzelm
# Date 1440016841 -7200
# Node ID e1159bd15982c62d94073bba445c23d3ead3bd44
# Parent  213bae1c075700902ad15c3345c6084ed9d281a4
repaired proofs after 6a6f15d8fbc4;

diff -r 213bae1c0757 -r e1159bd15982 src/HOL/Number_Theory/UniqueFactorization.thy
--- 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