--- a/src/HOL/RealDef.thy Mon May 10 12:12:58 2010 -0700
+++ b/src/HOL/RealDef.thy Mon May 10 14:53:33 2010 -0700
@@ -1045,6 +1045,7 @@
lemmas real_less_def = less_le [of "x::real" "y", standard]
lemmas real_abs_def = abs_real_def [of "r", standard]
lemmas real_sgn_def = sgn_real_def [of "x", standard]
+lemmas real_mult_commute = mult_commute [of "z::real" "w", standard]
lemmas real_mult_assoc = mult_assoc [of "z1::real" "z2" "z3", standard]
lemmas real_mult_1 = mult_1_left [of "z::real", standard]
lemmas real_add_mult_distrib = left_distrib [of "z1::real" "z2" "w", standard]