# HG changeset patch
# User huffman
# Date 1176234608 -7200
# Node ID 7a6c8ed516ab14745fb680ac2c684d64cd2c6158
# Parent  5fcee5b319a205e148c739fa8a91be9e9433c95f
removed unnecessary premise from power_le_imp_le_base

diff -r 5fcee5b319a2 -r 7a6c8ed516ab src/HOL/Power.thy
--- a/src/HOL/Power.thy	Tue Apr 10 18:09:58 2007 +0200
+++ b/src/HOL/Power.thy	Tue Apr 10 21:50:08 2007 +0200
@@ -291,8 +291,7 @@
 
 lemma power_le_imp_le_base:
   assumes le: "a ^ Suc n \<le> b ^ Suc n"
-      and xnonneg: "(0::'a::{ordered_semidom,recpower}) \<le> a"
-      and ynonneg: "0 \<le> b"
+      and ynonneg: "(0::'a::{ordered_semidom,recpower}) \<le> b"
   shows "a \<le> b"
  proof (rule ccontr)
    assume "~ a \<le> b"
diff -r 5fcee5b319a2 -r 7a6c8ed516ab src/HOL/Real/RealPow.thy
--- a/src/HOL/Real/RealPow.thy	Tue Apr 10 18:09:58 2007 +0200
+++ b/src/HOL/Real/RealPow.thy	Tue Apr 10 21:50:08 2007 +0200
@@ -228,7 +228,7 @@
 proof -
   from sq have "x ^ Suc (Suc 0) \<le> y ^ Suc (Suc 0)"
     by (simp only: numeral_2_eq_2)
-  thus "x \<le> y" using xgt0 ygt0
+  thus "x \<le> y" using ygt0
     by (rule power_le_imp_le_base)
 qed