| changeset 29223 | e09c53289830 |
| parent 28823 | dcbef866c9e2 |
| child 29252 | ea97aa6aeba2 |
--- a/src/HOL/Divides.thy Wed Dec 10 17:19:25 2008 +0100 +++ b/src/HOL/Divides.thy Thu Dec 11 18:30:26 2008 +0100 @@ -639,7 +639,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"] +class_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)"