diff -r 001d1aad99de -r 2e9a866141b8 src/HOL/RealPow.thy
--- a/src/HOL/RealPow.thy	Tue May 11 06:27:06 2010 -0700
+++ b/src/HOL/RealPow.thy	Tue May 11 06:30:48 2010 -0700
@@ -124,31 +124,4 @@
     by simp
 qed
 
-subsection {*Various Other Theorems*}
-
-lemma real_le_add_half_cancel: "(x + y/2 \<le> (y::real)) = (x \<le> y /2)"
-by auto
-
-lemma real_mult_inverse_cancel:
-     "[|(0::real) < x; 0 < x1; x1 * y < x * u |] 
-      ==> inverse x * y < inverse x1 * u"
-apply (rule_tac c=x in mult_less_imp_less_left) 
-apply (auto simp add: mult_assoc [symmetric])
-apply (simp (no_asm) add: mult_ac)
-apply (rule_tac c=x1 in mult_less_imp_less_right) 
-apply (auto simp add: mult_ac)
-done
-
-lemma real_mult_inverse_cancel2:
-     "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
-apply (auto dest: real_mult_inverse_cancel simp add: mult_ac)
-done
-
-(* TODO: no longer real-specific; rename and move elsewhere *)
-lemma realpow_num_eq_if:
-  fixes m :: "'a::power"
-  shows "m ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
-by (cases n, auto)
-
-
 end