# HG changeset patch
# User haftmann
# Date 1180687466 -7200
# Node ID f52b555f814168f36ffc5f1e01c6ba783ff7ebaf
# Parent  80b9caed2ba856e0de3bc45bdf0d3669a6b585b7
localized

diff -r 80b9caed2ba8 -r f52b555f8141 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Fri Jun 01 10:44:24 2007 +0200
+++ b/src/HOL/OrderedGroup.thy	Fri Jun 01 10:44:26 2007 +0200
@@ -42,9 +42,12 @@
 
 class ab_semigroup_mult = semigroup_mult +
   assumes mult_commute: "a \<^loc>* b = b \<^loc>* a"
+begin
 
-lemma mult_left_commute: "a * (b * c) = b * (a * (c::'a::ab_semigroup_mult))"
-  by (rule mk_left_commute [of "op *", OF mult_assoc mult_commute])
+lemma mult_left_commute: "a \<^loc>* (b \<^loc>* c) = b \<^loc>* (a \<^loc>* c)"
+  by (rule mk_left_commute [of "op \<^loc>*", OF mult_assoc mult_commute])
+
+end
 
 theorems mult_ac = mult_assoc mult_commute mult_left_commute