--- a/src/HOL/Divides.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Divides.thy Thu Mar 26 20:08:55 2009 +0100
@@ -852,7 +852,7 @@
text {* @{term "op dvd"} is a partial order *}
-interpretation dvd!: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"
+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 nat_dvd_diff[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"