src/HOL/GCD.thy
changeset 66816 212a3334e7da
parent 66803 dd8922885a68
child 66836 4eb431c3f974
     1.1 --- a/src/HOL/GCD.thy	Sun Oct 08 22:28:22 2017 +0200
     1.2 +++ b/src/HOL/GCD.thy	Sun Oct 08 22:28:22 2017 +0200
     1.3 @@ -2017,11 +2017,11 @@
     1.4  lemma gcd_non_0_int: "y > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
     1.5    for x y :: int
     1.6    apply (frule_tac b = y and a = x in pos_mod_sign)
     1.7 -  apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
     1.8 +  apply (simp del: Euclidean_Division.pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
     1.9    apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
    1.10    apply (frule_tac a = x in pos_mod_bound)
    1.11    apply (subst (1 2) gcd.commute)
    1.12 -  apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat nat_le_eq_zle)
    1.13 +  apply (simp del: Euclidean_Division.pos_mod_bound add: nat_diff_distrib gcd_diff2_nat nat_le_eq_zle)
    1.14    done
    1.15  
    1.16  lemma gcd_red_int: "gcd x y = gcd y (x mod y)"