--- a/src/HOL/Groups.thy Thu Feb 19 17:01:46 2015 +0000
+++ b/src/HOL/Groups.thy Thu Feb 19 16:32:53 2015 +0100
@@ -200,11 +200,11 @@
assumes add_0: "0 + a = a"
begin
-sublocale add!: comm_monoid plus 0
- by default (insert add_0, simp add: ac_simps)
+subclass monoid_add
+ by default (simp_all add: add_0 add.commute [of _ 0])
-subclass monoid_add
- by default (fact add.left_neutral add.right_neutral)+
+sublocale add!: comm_monoid plus 0
+ by default (simp add: ac_simps)
end
@@ -225,11 +225,11 @@
assumes mult_1: "1 * a = a"
begin
-sublocale mult!: comm_monoid times 1
- by default (insert mult_1, simp add: ac_simps)
+subclass monoid_mult
+ by default (simp_all add: mult_1 mult.commute [of _ 1])
-subclass monoid_mult
- by default (fact mult.left_neutral mult.right_neutral)+
+sublocale mult!: comm_monoid times 1
+ by default (simp add: ac_simps)
end