1.1 --- a/src/HOL/Power.thy	Tue Apr 10 18:09:58 2007 +0200
     1.2 +++ b/src/HOL/Power.thy	Tue Apr 10 21:50:08 2007 +0200
     1.3 @@ -291,8 +291,7 @@
     1.4  
     1.5  lemma power_le_imp_le_base:
     1.6    assumes le: "a ^ Suc n \<le> b ^ Suc n"
     1.7 -      and xnonneg: "(0::'a::{ordered_semidom,recpower}) \<le> a"
     1.8 -      and ynonneg: "0 \<le> b"
     1.9 +      and ynonneg: "(0::'a::{ordered_semidom,recpower}) \<le> b"
    1.10    shows "a \<le> b"
    1.11   proof (rule ccontr)
    1.12     assume "~ a \<le> b"