changeset 14387 e96d5c42c4b0 parent 14353 79f9fbef9106 child 14434 5f14c1207499
```     1.1 --- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Sat Feb 14 02:06:12 2004 +0100
1.2 +++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Sun Feb 15 10:46:37 2004 +0100
1.3 @@ -320,7 +320,7 @@
1.4    proof -;
1.5      assume "b \<le> q * a div p";
1.6      then have "p * b \<le> p * ((q * a) div p)";
1.7 -      by (insert p_g_2, auto simp add: zmult_zle_cancel1)
1.8 +      by (insert p_g_2, auto simp add: mult_le_cancel_left)
1.9      also have "... \<le> q * a";
1.10        by (rule zdiv_leq_prop, insert p_g_2, auto)
1.11      finally have "p * b \<le> q * a" .;
1.12 @@ -353,7 +353,7 @@
1.13    proof -;
1.14      assume "a \<le> p * b div q";
1.15      then have "q * a \<le> q * ((p * b) div q)";
1.16 -      by (insert q_g_2, auto simp add: zmult_zle_cancel1)
1.17 +      by (insert q_g_2, auto simp add: mult_le_cancel_left)
1.18      also have "... \<le> p * b";
1.19        by (rule zdiv_leq_prop, insert q_g_2, auto)
1.20      finally have "q * a \<le> p * b" .;
1.21 @@ -425,7 +425,7 @@
1.22          assume "0 < x" and "x \<le> q * j div p";
1.23          with j_fact P_set_def  have "j \<le> (p - 1) div 2"; by auto
1.24          with q_g_2; have "q * j \<le> q * ((p - 1) div 2)";
1.25 -          by (auto simp add: zmult_zle_cancel1)
1.26 +          by (auto simp add: mult_le_cancel_left)
1.27          with p_g_2 have "q * j div p \<le> q * ((p - 1) div 2) div p";
1.28            by (auto simp add: zdiv_mono1)
1.29          also from prems have "... \<le> (q - 1) div 2";
1.30 @@ -437,7 +437,7 @@
1.31    also have "... = (q * j) div p";
1.32    proof -;
1.33      from j_fact P_set_def have "0 \<le> j" by auto
1.34 -    with q_g_2 have "q * 0 \<le> q * j" by (auto simp only: zmult_zle_mono2)
1.35 +    with q_g_2 have "q * 0 \<le> q * j" by (auto simp only: mult_left_mono)
1.36      then have "0 \<le> q * j" by auto
1.37      then have "0 div p \<le> (q * j) div p";
1.38        apply (rule_tac a = 0 in zdiv_mono1)
1.39 @@ -478,7 +478,7 @@
1.40          assume "0 < x" and "x \<le> p * j div q";
1.41          with j_fact Q_set_def  have "j \<le> (q - 1) div 2"; by auto
1.42          with p_g_2; have "p * j \<le> p * ((q - 1) div 2)";
1.43 -          by (auto simp add: zmult_zle_cancel1)
1.44 +          by (auto simp add: mult_le_cancel_left)
1.45          with q_g_2 have "p * j div q \<le> p * ((q - 1) div 2) div q";
1.46            by (auto simp add: zdiv_mono1)
1.47          also from prems have "... \<le> (p - 1) div 2";
1.48 @@ -490,7 +490,7 @@
1.49    also have "... = (p * j) div q";
1.50    proof -;
1.51      from j_fact Q_set_def have "0 \<le> j" by auto
1.52 -    with p_g_2 have "p * 0 \<le> p * j" by (auto simp only: zmult_zle_mono2)
1.53 +    with p_g_2 have "p * 0 \<le> p * j" by (auto simp only: mult_left_mono)
1.54      then have "0 \<le> p * j" by auto
1.55      then have "0 div q \<le> (p * j) div q";
1.56        apply (rule_tac a = 0 in zdiv_mono1)
```