# HG changeset patch
# User huffman
# Date 1334208794 -7200
# Node ID 45b58fec9024f59539020c3507fe0e642d2e3632
# Parent  0daa97ed158529f598737f6381048227db6874dd
remove outdated comment

diff -r 0daa97ed1585 -r 45b58fec9024 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Wed Apr 11 21:40:46 2012 +0200
+++ b/src/HOL/RealDef.thy	Thu Apr 12 07:33:14 2012 +0200
@@ -1058,8 +1058,7 @@
 by simp (* solved by linordered_ring_le_cancel_factor simproc *)
 
 lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
-by (rule mult_le_cancel_left_pos)
-(* BH: Why doesn't "simp" prove this one, like it does the last one? *)
+by simp (* solved by linordered_ring_le_cancel_factor simproc *)
 
 
 subsection {* Embedding numbers into the Reals *}