src/HOL/NumberTheory/Quadratic_Reciprocity.thy
changeset 14353 79f9fbef9106
parent 13871 26e5f5e624f6
child 14387 e96d5c42c4b0
     1.1 --- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Mon Jan 12 16:45:35 2004 +0100
     1.2 +++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Mon Jan 12 16:51:45 2004 +0100
     1.3 @@ -130,7 +130,7 @@
     1.4          then have "0 \<le> x";
     1.5            by (auto simp add: A_def)
     1.6          with a_nonzero have "0 \<le> x * a";
     1.7 -          by (auto simp add: int_0_le_mult_iff)
     1.8 +          by (auto simp add: zero_le_mult_iff)
     1.9          with p_g_2 show "0 \<le> x * a div p"; 
    1.10            by (auto simp add: pos_imp_zdiv_nonneg_iff)
    1.11        qed;