localized
authorhaftmann
Fri Jun 01 10:44:26 2007 +0200 (2007-06-01)
changeset 23181f52b555f8141
parent 23180 80b9caed2ba8
child 23182 01fa88b79ddc
localized
src/HOL/OrderedGroup.thy
     1.1 --- a/src/HOL/OrderedGroup.thy	Fri Jun 01 10:44:24 2007 +0200
     1.2 +++ b/src/HOL/OrderedGroup.thy	Fri Jun 01 10:44:26 2007 +0200
     1.3 @@ -42,9 +42,12 @@
     1.4  
     1.5  class ab_semigroup_mult = semigroup_mult +
     1.6    assumes mult_commute: "a \<^loc>* b = b \<^loc>* a"
     1.7 +begin
     1.8  
     1.9 -lemma mult_left_commute: "a * (b * c) = b * (a * (c::'a::ab_semigroup_mult))"
    1.10 -  by (rule mk_left_commute [of "op *", OF mult_assoc mult_commute])
    1.11 +lemma mult_left_commute: "a \<^loc>* (b \<^loc>* c) = b \<^loc>* (a \<^loc>* c)"
    1.12 +  by (rule mk_left_commute [of "op \<^loc>*", OF mult_assoc mult_commute])
    1.13 +
    1.14 +end
    1.15  
    1.16  theorems mult_ac = mult_assoc mult_commute mult_left_commute
    1.17