--- a/src/HOL/Groups.thy Tue Oct 06 13:31:44 2015 +0200
+++ b/src/HOL/Groups.thy Tue Oct 06 15:14:28 2015 +0200
@@ -147,13 +147,13 @@
declare add.left_commute [algebra_simps, field_simps]
-theorems add_ac = add.assoc add.commute add.left_commute
+lemmas add_ac = add.assoc add.commute add.left_commute
end
hide_fact add_commute
-theorems add_ac = add.assoc add.commute add.left_commute
+lemmas 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)"
@@ -175,13 +175,13 @@
declare mult.left_commute [algebra_simps, field_simps]
-theorems mult_ac = mult.assoc mult.commute mult.left_commute
+lemmas mult_ac = mult.assoc mult.commute mult.left_commute
end
hide_fact mult_commute
-theorems mult_ac = mult.assoc mult.commute mult.left_commute
+lemmas mult_ac = mult.assoc mult.commute mult.left_commute
class monoid_add = zero + semigroup_add +
assumes add_0_left: "0 + a = a"