reinstated popular add_ac and mult_ac to avoid needless incompatibilities in user space
authornipkow
Fri Jul 18 14:21:42 2014 +0200 (2014-07-18)
changeset 57571d38a98f496dd
parent 57570 70fcc6428393
child 57572 57932dd40916
reinstated popular add_ac and mult_ac to avoid needless incompatibilities in user space
src/HOL/Groups.thy
     1.1 --- a/src/HOL/Groups.thy	Fri Jul 18 14:03:09 2014 +0200
     1.2 +++ b/src/HOL/Groups.thy	Fri Jul 18 14:21:42 2014 +0200
     1.3 @@ -169,10 +169,14 @@
     1.4  
     1.5  declare add.left_commute [algebra_simps, field_simps]
     1.6  
     1.7 +theorems add_ac = add.assoc add.commute add.left_commute
     1.8 +
     1.9  end
    1.10  
    1.11  hide_fact add_commute
    1.12  
    1.13 +theorems add_ac = add.assoc add.commute add.left_commute
    1.14 +
    1.15  class semigroup_mult = times +
    1.16    assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"
    1.17  begin
    1.18 @@ -193,10 +197,14 @@
    1.19  
    1.20  declare mult.left_commute [algebra_simps, field_simps]
    1.21  
    1.22 +theorems mult_ac = mult.assoc mult.commute mult.left_commute
    1.23 +
    1.24  end
    1.25  
    1.26  hide_fact mult_commute
    1.27  
    1.28 +theorems mult_ac = mult.assoc mult.commute mult.left_commute
    1.29 +
    1.30  class monoid_add = zero + semigroup_add +
    1.31    assumes add_0_left: "0 + a = a"
    1.32      and add_0_right: "a + 0 = a"