src/HOL/NumberTheory/IntPrimes.thy
changeset 14353 79f9fbef9106
parent 14271 8ed6989228bb
child 14378 69c4d5997669
     1.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Mon Jan 12 16:45:35 2004 +0100
     1.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Mon Jan 12 16:51:45 2004 +0100
     1.3 @@ -126,7 +126,7 @@
     1.4  lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd (m, n) = zgcd (k * m, k * n)"
     1.5    by (simp del: zmult_zminus_right
     1.6        add: zmult_zminus_right [symmetric] nat_mult_distrib zgcd_def zabs_def
     1.7 -          zmult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric])
     1.8 +          mult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric])
     1.9  
    1.10  lemma zgcd_zmult_distrib2_abs: "zgcd (k * m, k * n) = abs k * zgcd (m, n)"
    1.11    by (simp add: zabs_def zgcd_zmult_distrib2)
    1.12 @@ -144,7 +144,7 @@
    1.13       "zgcd (n, k) = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m"
    1.14    apply (subgoal_tac "m = zgcd (m * n, m * k)")
    1.15     apply (erule ssubst, rule zgcd_greatest_iff [THEN iffD2])
    1.16 -   apply (simp_all add: zgcd_zmult_distrib2 [symmetric] int_0_le_mult_iff)
    1.17 +   apply (simp_all add: zgcd_zmult_distrib2 [symmetric] zero_le_mult_iff)
    1.18    done
    1.19  
    1.20  lemma zrelprime_zdvd_zmult: "zgcd (n, k) = 1 ==> k dvd m * n ==> k dvd m"
    1.21 @@ -363,7 +363,7 @@
    1.22      "0 \<le> a ==> a < m ==> [a = 0] (mod m) ==> a = 0"
    1.23    apply (unfold zcong_def dvd_def, auto)
    1.24    apply (subgoal_tac "0 < m")
    1.25 -   apply (simp add: int_0_le_mult_iff)
    1.26 +   apply (simp add: zero_le_mult_iff)
    1.27     apply (subgoal_tac "m * k < m * 1")
    1.28      apply (drule zmult_zless_cancel1 [THEN iffD1])
    1.29      apply (auto simp add: linorder_neq_iff)