src/HOL/GCD.thy
changeset 63915 bab633745c7f
parent 63882 018998c00003
child 63924 f91766530e13
--- a/src/HOL/GCD.thy	Sun Sep 18 17:59:28 2016 +0200
+++ b/src/HOL/GCD.thy	Sun Sep 18 20:33:48 2016 +0200
@@ -860,10 +860,7 @@
   by (subst add_commute) simp
 
 lemma setprod_coprime [rule_format]: "(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1"
-  apply (cases "finite A")
-   apply (induct set: finite)
-    apply (auto simp add: gcd_mult_cancel)
-  done
+  by (induct A rule: infinite_finite_induct) (auto simp add: gcd_mult_cancel)
 
 lemma prod_list_coprime: "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (prod_list xs) y"
   by (induct xs) (simp_all add: gcd_mult_cancel)