src/HOL/Power.thy
changeset 41550 efa734d9b221
parent 39438 c5ece2a7a86e
child 45231 d85a2fdc586c
     1.1 --- a/src/HOL/Power.thy	Fri Jan 14 15:43:04 2011 +0100
     1.2 +++ b/src/HOL/Power.thy	Fri Jan 14 15:44:47 2011 +0100
     1.3 @@ -297,7 +297,7 @@
     1.4    assume "~ a \<le> b"
     1.5    then have "b < a" by (simp only: linorder_not_le)
     1.6    then have "b ^ Suc n < a ^ Suc n"
     1.7 -    by (simp only: prems power_strict_mono)
     1.8 +    by (simp only: assms power_strict_mono)
     1.9    from le and this show False
    1.10      by (simp add: linorder_not_less [symmetric])
    1.11  qed