src/HOL/GCD.thy
changeset 61954 1d43f86f48be
parent 61944 5d06ecfdb472
child 61975 b4b11391c676
     1.1 --- a/src/HOL/GCD.thy	Mon Dec 28 18:03:26 2015 +0100
     1.2 +++ b/src/HOL/GCD.thy	Mon Dec 28 19:23:15 2015 +0100
     1.3 @@ -1489,14 +1489,14 @@
     1.4      gcd_commute_int [of "n - 1" n] by auto
     1.5  
     1.6  lemma setprod_coprime_nat [rule_format]:
     1.7 -    "(ALL i: A. coprime (f i) (x::nat)) --> coprime (PROD i:A. f i) x"
     1.8 +    "(ALL i: A. coprime (f i) (x::nat)) --> coprime (\<Prod>i\<in>A. f i) x"
     1.9    apply (case_tac "finite A")
    1.10    apply (induct set: finite)
    1.11    apply (auto simp add: gcd_mult_cancel_nat)
    1.12  done
    1.13  
    1.14  lemma setprod_coprime_int [rule_format]:
    1.15 -    "(ALL i: A. coprime (f i) (x::int)) --> coprime (PROD i:A. f i) x"
    1.16 +    "(ALL i: A. coprime (f i) (x::int)) --> coprime (\<Prod>i\<in>A. f i) x"
    1.17    apply (case_tac "finite A")
    1.18    apply (induct set: finite)
    1.19    apply (auto simp add: gcd_mult_cancel_int)