# HG changeset patch
# User nipkow
# Date 1405686102 -7200
# Node ID d38a98f496ddbcae13f423aed91ea275370b8e7e
# Parent  70fcc642839300ab5955605822fc1703211cc2f9
reinstated popular add_ac and mult_ac to avoid needless incompatibilities in user space

diff -r 70fcc6428393 -r d38a98f496dd src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Fri Jul 18 14:03:09 2014 +0200
+++ b/src/HOL/Groups.thy	Fri Jul 18 14:21:42 2014 +0200
@@ -169,10 +169,14 @@
 
 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
@@ -193,10 +197,14 @@
 
 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"