--- a/src/HOL/Divides.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Divides.thy Mon Nov 17 17:00:55 2008 +0100
@@ -639,8 +639,8 @@
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