# HG changeset patch
# User haftmann
# Date 1712861209 0
# Node ID 5ed992c47cdc2d0b672f2215a9a1ed869ae35f88
# Parent  83fa23ca40e55c7a8f5e4d539b55ac103d1391dd
prefer canonical theorem name for fact collection declarations

diff -r 83fa23ca40e5 -r 5ed992c47cdc src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Fri Apr 12 09:58:53 2024 +0100
+++ b/src/HOL/Groups.thy	Thu Apr 11 18:46:49 2024 +0000
@@ -207,26 +207,27 @@
 subsection \<open>Semigroups and Monoids\<close>
 
 class semigroup_add = plus +
-  assumes add_assoc [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
-    "(a + b) + c = a + (b + c)"
+  assumes add_assoc: "(a + b) + c = a + (b + c)"
 begin
 
 sublocale add: semigroup plus
   by standard (fact add_assoc)
 
+declare add.assoc [algebra_simps, algebra_split_simps, field_simps, field_split_simps]
+
 end
 
 hide_fact add_assoc
 
 class ab_semigroup_add = semigroup_add +
-  assumes add_commute [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
-    "a + b = b + a"
+  assumes add_commute: "a + b = b + a"
 begin
 
 sublocale add: abel_semigroup plus
   by standard (fact add_commute)
 
-declare add.left_commute [algebra_simps, algebra_split_simps, field_simps, field_split_simps]
+declare add.commute [algebra_simps, algebra_split_simps, field_simps, field_split_simps]
+  add.left_commute [algebra_simps, algebra_split_simps, field_simps, field_split_simps]
 
 lemmas add_ac = add.assoc add.commute add.left_commute
 
@@ -237,26 +238,27 @@
 lemmas add_ac = add.assoc add.commute add.left_commute
 
 class semigroup_mult = times +
-  assumes mult_assoc [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
-    "(a * b) * c = a * (b * c)"
+  assumes mult_assoc: "(a * b) * c = a * (b * c)"
 begin
 
 sublocale mult: semigroup times
   by standard (fact mult_assoc)
 
+declare mult.assoc [algebra_simps, algebra_split_simps, field_simps, field_split_simps]
+
 end
 
 hide_fact mult_assoc
 
 class ab_semigroup_mult = semigroup_mult +
-  assumes mult_commute [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
-    "a * b = b * a"
+  assumes mult_commute: "a * b = b * a"
 begin
 
 sublocale mult: abel_semigroup times
   by standard (fact mult_commute)
 
-declare mult.left_commute [algebra_simps, algebra_split_simps, field_simps, field_split_simps]
+declare mult.commute [algebra_simps, algebra_split_simps, field_simps, field_split_simps]
+  mult.left_commute [algebra_simps, algebra_split_simps, field_simps, field_split_simps]
 
 lemmas mult_ac = mult.assoc mult.commute mult.left_commute