src/HOL/OrderedGroup.thy

   hence "0 <= a+a" by (simp add: add_mono[OF a a, simplified])
   hence "~(a+a < 0)" by simp
   with a show ?thesis by simp 
 qed
 
-class lordered_ab_group_abs = lordered_ab_group +
+class lordered_ab_group_abs = lordered_ab_group + abs +
   assumes abs_lattice: "abs x = sup x (uminus x)"
 
 lemma abs_zero[simp]: "abs 0 = (0::'a::lordered_ab_group_abs)"
 by (simp add: abs_lattice)