src/HOL/Power.thy
changeset 61076 bdc1e2f0a86a
parent 60974 6a6f15d8fbc4
child 61378 3e04c9ca001a
     1.1 --- a/src/HOL/Power.thy	Tue Sep 01 17:25:36 2015 +0200
     1.2 +++ b/src/HOL/Power.thy	Tue Sep 01 22:32:58 2015 +0200
     1.3 @@ -800,7 +800,7 @@
     1.4  Premises cannot be weakened: consider the case where @{term "i=0"},
     1.5  @{term "m=1"} and @{term "n=0"}.\<close>
     1.6  lemma nat_power_less_imp_less:
     1.7 -  assumes nonneg: "0 < (i\<Colon>nat)"
     1.8 +  assumes nonneg: "0 < (i::nat)"
     1.9    assumes less: "i ^ m < i ^ n"
    1.10    shows "m < n"
    1.11  proof (cases "i = 1")