src/HOL/Groups.thy
changeset 59559 35da1bbf234e
parent 59557 ebd8ecacfba6
child 59815 cce82e360c2f
     1.1 --- a/src/HOL/Groups.thy	Thu Feb 19 17:01:46 2015 +0000
     1.2 +++ b/src/HOL/Groups.thy	Thu Feb 19 16:32:53 2015 +0100
     1.3 @@ -200,11 +200,11 @@
     1.4    assumes add_0: "0 + a = a"
     1.5  begin
     1.6  
     1.7 -sublocale add!: comm_monoid plus 0
     1.8 -  by default (insert add_0, simp add: ac_simps)
     1.9 +subclass monoid_add
    1.10 +  by default (simp_all add: add_0 add.commute [of _ 0])
    1.11  
    1.12 -subclass monoid_add
    1.13 -  by default (fact add.left_neutral add.right_neutral)+
    1.14 +sublocale add!: comm_monoid plus 0
    1.15 +  by default (simp add: ac_simps)
    1.16  
    1.17  end
    1.18  
    1.19 @@ -225,11 +225,11 @@
    1.20    assumes mult_1: "1 * a = a"
    1.21  begin
    1.22  
    1.23 -sublocale mult!: comm_monoid times 1
    1.24 -  by default (insert mult_1, simp add: ac_simps)
    1.25 +subclass monoid_mult
    1.26 +  by default (simp_all add: mult_1 mult.commute [of _ 1])
    1.27  
    1.28 -subclass monoid_mult
    1.29 -  by default (fact mult.left_neutral mult.right_neutral)+
    1.30 +sublocale mult!: comm_monoid times 1
    1.31 +  by default (simp add: ac_simps)
    1.32  
    1.33  end
    1.34