src/HOL/OrderedGroup.thy
changeset 23181 f52b555f8141
parent 23085 fd30d75a6614
child 23389 aaca6a8e5414
     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