diff -r 76ff0a15d202 -r dc429a5b13c4 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Wed Mar 19 14:55:47 2014 +0000
+++ b/src/HOL/Real.thy	Wed Mar 19 17:06:02 2014 +0000
@@ -974,12 +974,6 @@
 text {* BH: These lemmas should not be necessary; they should be
 covered by existing simp rules and simplification procedures. *}
 
-lemma real_mult_left_cancel: "(c::real) \<noteq> 0 ==> (c*a=c*b) = (a=b)"
-by simp (* redundant with mult_cancel_left *)
-
-lemma real_mult_right_cancel: "(c::real) \<noteq> 0 ==> (a*c=b*c) = (a=b)"
-by simp (* redundant with mult_cancel_right *)
-
 lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)"
 by simp (* solved by linordered_ring_less_cancel_factor simproc *)