--- 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