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