src/HOL/Divides.thy

   unfolding dvd_def
   by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
 
 text {* @{term "op dvd"} is a partial order *}
 
-interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> n \<noteq> m"]
-  by unfold_locales (auto intro: dvd_refl dvd_trans dvd_anti_sym)
+interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"]
+  proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
 
 lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
   unfolding dvd_def
   by (blast intro: diff_mult_distrib2 [symmetric])