--- a/src/HOL/Groups.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Groups.thy Sat Jul 05 11:01:53 2014 +0200
@@ -169,14 +169,10 @@
declare add.left_commute [algebra_simps, field_simps]
-theorems add_ac = add.assoc add.commute add.left_commute
-
end
hide_fact add_commute
-theorems add_ac = add.assoc add.commute add.left_commute
-
class semigroup_mult = times +
assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"
begin
@@ -197,14 +193,10 @@
declare mult.left_commute [algebra_simps, field_simps]
-theorems mult_ac = mult.assoc mult.commute mult.left_commute
-
end
hide_fact mult_commute
-theorems mult_ac = mult.assoc mult.commute mult.left_commute
-
class monoid_add = zero + semigroup_add +
assumes add_0_left: "0 + a = a"
and add_0_right: "a + 0 = a"