# HG changeset patch
# User nipkow
# Date 1179041007 -7200
# Node ID 2863582c61b5f521626d4b8456d7ecbc96b1d7ef
# Parent  1d471b8dec4ee0a5c5d2e8d9f0706833a078fad8
Removed junk

diff -r 1d471b8dec4e -r 2863582c61b5 src/HOL/Real/RealPow.thy
--- a/src/HOL/Real/RealPow.thy	Sun May 13 07:11:21 2007 +0200
+++ b/src/HOL/Real/RealPow.thy	Sun May 13 09:23:27 2007 +0200
@@ -235,14 +235,4 @@
 lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
 by (case_tac "n", auto)
 
-lemma real_num_zero_less_two_pow [simp]: "0 < (2::real) ^ (4*d)"
-by (simp add: zero_less_power)
-
-lemma lemma_realpow_num_two_mono:
-     "x * (4::real)   < y ==> x * (2 ^ 8) < y * (2 ^ 6)"
-apply (subgoal_tac " (2::real) ^ 8 = 4 * (2 ^ 6) ")
-apply (simp (no_asm_simp) add: real_mult_assoc [symmetric])
-apply (auto simp add: realpow_num_eq_if)
-done
-
 end