remove redundant lemma real_minus_half_eq

--- a/src/HOL/RealPow.thy	Wed Feb 24 10:36:17 2010 -0800
+++ b/src/HOL/RealPow.thy	Wed Feb 24 14:13:15 2010 -0800
@@ -113,9 +113,6 @@
 lemma real_le_add_half_cancel: "(x + y/2 \<le> (y::real)) = (x \<le> y /2)"
 by auto
 
-lemma real_minus_half_eq [simp]: "(x::real) - x/2 = x/2"
-by auto
-
 lemma real_mult_inverse_cancel:
      "[|(0::real) < x; 0 < x1; x1 * y < x * u |] 
       ==> inverse x * y < inverse x1 * u"