# HG changeset patch
# User huffman
# Date 1267049595 28800
# Node ID 992f9cb60b25cbb2ddd434a7e45e1344b8409ccc
# Parent  ae742caa0c5bfd036d59d948fd6dfa03daba5851
remove redundant lemma real_minus_half_eq

diff -r ae742caa0c5b -r 992f9cb60b25 src/HOL/RealPow.thy
--- 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"