# HG changeset patch
# User huffman
# Date 1266965064 28800
# Node ID c6331256b087d736b8f3ec15fb0d6d53ea40e626
# Parent  be0c69c06176c434197eea8aa82f27310c0d0589
remove redundant lemma realpow_increasing

diff -r be0c69c06176 -r c6331256b087 src/HOL/RealPow.thy
--- a/src/HOL/RealPow.thy	Tue Feb 23 14:38:06 2010 -0800
+++ b/src/HOL/RealPow.thy	Tue Feb 23 14:44:24 2010 -0800
@@ -42,11 +42,6 @@
 apply auto
 done
 
-(* used by AFP Integration theory *)
-lemma realpow_increasing:
-     "[|(0::real) \<le> x; 0 \<le> y; x ^ Suc n \<le> y ^ Suc n|] ==> x \<le> y"
-  by (rule power_le_imp_le_base)
-
 
 subsection{* Squares of Reals *}