
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




