changeset 15923 | 01d5d0c1c078 |
parent 15542 | ee6cd48cf840 |
child 16417 | 9bc16273c2d4 |
--- 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':