src/HOL/Real/RealDef.thy
changeset 15923 01d5d0c1c078
parent 15542 ee6cd48cf840
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/Real/RealDef.thy	Wed May 04 08:37:45 2005 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Wed May 04 10:42:43 2005 +0200
     1.3 @@ -587,8 +587,7 @@
     1.4  done
     1.5  
     1.6  lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
     1.7 -  by (force elim: order_less_asym
     1.8 -            simp add: Ring_and_Field.mult_le_cancel_left)
     1.9 +by(simp add:mult_commute)
    1.10  
    1.11  text{*Only two uses?*}
    1.12  lemma real_mult_less_mono':