src/HOL/Real/RealDef.thy

--- a/src/HOL/Real/RealDef.thy	Wed May 04 08:37:45 2005 +0200
+++ b/src/HOL/Real/RealDef.thy	Wed May 04 10:42:43 2005 +0200
@@ -587,8 +587,7 @@
 done
 
 lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
-  by (force elim: order_less_asym
-            simp add: Ring_and_Field.mult_le_cancel_left)
+by(simp add:mult_commute)
 
 text{*Only two uses?*}
 lemma real_mult_less_mono':