# HG changeset patch
# User huffman
# Date 1273528413 25200
# Node ID d75a28a13639e21ae91432d113bbee4c05612bb9
# Parent  e05e1283c550f1a3d64269430b1458e9c5ba1862
add real_mult_commute to legacy theorem names

diff -r e05e1283c550 -r d75a28a13639 src/HOL/RealDef.thy
--- 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]