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"