diff -r 466e714de2fc -r c03e9d04b3e4 src/HOL/OrderedGroup.thy --- a/src/HOL/OrderedGroup.thy Wed Jan 02 12:22:38 2008 +0100 +++ b/src/HOL/OrderedGroup.thy Wed Jan 02 15:14:02 2008 +0100 @@ -121,7 +121,7 @@ subsection {* Groups *} -class group_add = minus + monoid_add + +class group_add = minus + uminus + monoid_add + assumes left_minus [simp]: "- a + a = 0" assumes diff_minus: "a - b = a + (- b)" begin @@ -219,7 +219,7 @@ end -class ab_group_add = minus + comm_monoid_add + +class ab_group_add = minus + uminus + comm_monoid_add + assumes ab_left_minus: "- a + a = 0" assumes ab_diff_minus: "a - b = a + (- b)" begin