diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/NumberTheory/IntPrimes.thy --- a/src/HOL/NumberTheory/IntPrimes.thy Mon Jan 12 16:45:35 2004 +0100 +++ b/src/HOL/NumberTheory/IntPrimes.thy Mon Jan 12 16:51:45 2004 +0100 @@ -126,7 +126,7 @@ lemma zgcd_zmult_distrib2: "0 \ k ==> k * zgcd (m, n) = zgcd (k * m, k * n)" by (simp del: zmult_zminus_right add: zmult_zminus_right [symmetric] nat_mult_distrib zgcd_def zabs_def - zmult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric]) + mult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric]) lemma zgcd_zmult_distrib2_abs: "zgcd (k * m, k * n) = abs k * zgcd (m, n)" by (simp add: zabs_def zgcd_zmult_distrib2) @@ -144,7 +144,7 @@ "zgcd (n, k) = 1 ==> k dvd m * n ==> 0 \ m ==> k dvd m" apply (subgoal_tac "m = zgcd (m * n, m * k)") apply (erule ssubst, rule zgcd_greatest_iff [THEN iffD2]) - apply (simp_all add: zgcd_zmult_distrib2 [symmetric] int_0_le_mult_iff) + apply (simp_all add: zgcd_zmult_distrib2 [symmetric] zero_le_mult_iff) done lemma zrelprime_zdvd_zmult: "zgcd (n, k) = 1 ==> k dvd m * n ==> k dvd m" @@ -363,7 +363,7 @@ "0 \ a ==> a < m ==> [a = 0] (mod m) ==> a = 0" apply (unfold zcong_def dvd_def, auto) apply (subgoal_tac "0 < m") - apply (simp add: int_0_le_mult_iff) + apply (simp add: zero_le_mult_iff) apply (subgoal_tac "m * k < m * 1") apply (drule zmult_zless_cancel1 [THEN iffD1]) apply (auto simp add: linorder_neq_iff)