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