src/HOL/IntDef.thy

 lemma zmult_zless_mono2: "[| i<j;  (0::int) < k |] ==> k*i < k*j"
 apply (drule zero_less_imp_eq_int)
 apply (auto simp add: zmult_zless_mono2_lemma)
 done
 
-instance int :: minus
+instance int :: abs
   zabs_def: "\<bar>i\<Colon>int\<bar> \<equiv> if i < 0 then - i else i" ..
 
 instance int :: distrib_lattice
   "inf \<equiv> min"
   "sup \<equiv> max"