src/HOL/OrderedGroup.thy
changeset 23879 4776af8be741
parent 23477 f4b83f03cac9
child 24137 8d7896398147
     1.1 --- a/src/HOL/OrderedGroup.thy	Fri Jul 20 14:27:56 2007 +0200
     1.2 +++ b/src/HOL/OrderedGroup.thy	Fri Jul 20 14:28:01 2007 +0200
     1.3 @@ -783,7 +783,7 @@
     1.4    with a show ?thesis by simp 
     1.5  qed
     1.6  
     1.7 -class lordered_ab_group_abs = lordered_ab_group +
     1.8 +class lordered_ab_group_abs = lordered_ab_group + abs +
     1.9    assumes abs_lattice: "abs x = sup x (uminus x)"
    1.10  
    1.11  lemma abs_zero[simp]: "abs 0 = (0::'a::lordered_ab_group_abs)"