src/HOL/Divides.thy
changeset 16796 140f1e0ea846
parent 16733 236dfafbeb63
child 17084 fb0a80aef0be
     1.1 --- a/src/HOL/Divides.thy	Wed Jul 13 15:06:04 2005 +0200
     1.2 +++ b/src/HOL/Divides.thy	Wed Jul 13 15:06:20 2005 +0200
     1.3 @@ -82,7 +82,7 @@
     1.4  
     1.5  (*Avoids the ugly ~m<n above*)
     1.6  lemma le_mod_geq: "(n::nat) \<le> m ==> m mod n = (m-n) mod n"
     1.7 -by (simp add: mod_geq not_less_iff_le)
     1.8 +by (simp add: mod_geq linorder_not_less)
     1.9  
    1.10  lemma mod_if: "m mod (n::nat) = (if m<n then m else (m-n) mod n)"
    1.11  by (simp add: mod_geq)
    1.12 @@ -149,7 +149,7 @@
    1.13  
    1.14  (*Avoids the ugly ~m<n above*)
    1.15  lemma le_div_geq: "[| 0<n;  n\<le>m |] ==> m div n = Suc((m-n) div n)"
    1.16 -by (simp add: div_geq not_less_iff_le)
    1.17 +by (simp add: div_geq linorder_not_less)
    1.18  
    1.19  lemma div_if: "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))"
    1.20  by (simp add: div_geq)
    1.21 @@ -483,7 +483,7 @@
    1.22  (* case Suc(na) < n *)
    1.23  apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
    1.24  (* case n \<le> Suc(na) *)
    1.25 -apply (simp add: not_less_iff_le le_Suc_eq mod_geq)
    1.26 +apply (simp add: linorder_not_less le_Suc_eq mod_geq)
    1.27  apply (auto simp add: Suc_diff_le le_mod_geq)
    1.28  done
    1.29  
    1.30 @@ -545,7 +545,7 @@
    1.31  done
    1.32  
    1.33  lemma dvd_diffD: "[| k dvd m-n; k dvd n; n\<le>m |] ==> k dvd (m::nat)"
    1.34 -apply (erule not_less_iff_le [THEN iffD2, THEN add_diff_inverse, THEN subst])
    1.35 +apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
    1.36  apply (blast intro: dvd_add)
    1.37  done
    1.38