changeset 13483 | 0e6adce08fb0 |
parent 13476 | 600f1c93124f |
child 14260 | 3862336cd4bd |
--- a/src/HOL/Library/Ring_and_Field.thy Thu Aug 08 23:47:41 2002 +0200 +++ b/src/HOL/Library/Ring_and_Field.thy Thu Aug 08 23:48:31 2002 +0200 @@ -90,7 +90,7 @@ qed lemma mult_left_commute: "a * (b * c) = b * (a * (c::'a::ring))" -by(rule mk_left_commute[OF mult_assoc mult_commute]) + by (rule mk_left_commute [of "op *", OF mult_assoc mult_commute]) theorems ring_mult_ac = mult_assoc mult_commute mult_left_commute