src/HOL/Divides.thy
changeset 29223 e09c53289830
parent 28823 dcbef866c9e2
child 29252 ea97aa6aeba2
     1.1 --- a/src/HOL/Divides.thy	Wed Dec 10 17:19:25 2008 +0100
     1.2 +++ b/src/HOL/Divides.thy	Thu Dec 11 18:30:26 2008 +0100
     1.3 @@ -639,7 +639,7 @@
     1.4  
     1.5  text {* @{term "op dvd"} is a partial order *}
     1.6  
     1.7 -interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"]
     1.8 +class_interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"]
     1.9    proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
    1.10  
    1.11  lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"