src/HOL/Real/RealPow.thy
changeset 22624 7a6c8ed516ab
parent 20634 45fe31e72391
child 22945 2863582c61b5
     1.1 --- a/src/HOL/Real/RealPow.thy	Tue Apr 10 18:09:58 2007 +0200
     1.2 +++ b/src/HOL/Real/RealPow.thy	Tue Apr 10 21:50:08 2007 +0200
     1.3 @@ -228,7 +228,7 @@
     1.4  proof -
     1.5    from sq have "x ^ Suc (Suc 0) \<le> y ^ Suc (Suc 0)"
     1.6      by (simp only: numeral_2_eq_2)
     1.7 -  thus "x \<le> y" using xgt0 ygt0
     1.8 +  thus "x \<le> y" using ygt0
     1.9      by (rule power_le_imp_le_base)
    1.10  qed
    1.11