src/HOL/Nat.thy
changeset 62344 759d684c0e60
parent 62326 3cf7a067599c
child 62365 8a105c235b1f
     1.1 --- a/src/HOL/Nat.thy	Wed Feb 17 21:51:56 2016 +0100
     1.2 +++ b/src/HOL/Nat.thy	Wed Feb 17 21:51:56 2016 +0100
     1.3 @@ -1934,11 +1934,6 @@
     1.4    unfolding dvd_def
     1.5    by (force dest: mult_eq_self_implies_10 simp add: mult.assoc)
     1.6  
     1.7 -text \<open>@{term "op dvd"} is a partial order\<close>
     1.8 -
     1.9 -interpretation dvd: order "op dvd" "\<lambda>n m :: nat. n dvd m \<and> \<not> m dvd n"
    1.10 -  proof qed (auto intro: dvd_refl dvd_trans dvd_antisym)
    1.11 -
    1.12  lemma dvd_diff_nat[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
    1.13  unfolding dvd_def
    1.14  by (blast intro: diff_mult_distrib2 [symmetric])