src/HOL/Power.thy
changeset 31021 53642251a04f
parent 31001 7e6ffd8f51a9
child 31155 92d8ff6af82c
     1.1 --- a/src/HOL/Power.thy	Tue Apr 28 19:15:50 2009 +0200
     1.2 +++ b/src/HOL/Power.thy	Wed Apr 29 14:20:26 2009 +0200
     1.3 @@ -419,13 +419,9 @@
     1.4  apply assumption
     1.5  done
     1.6  
     1.7 -class recpower = monoid_mult
     1.8 -
     1.9  
    1.10  subsection {* Exponentiation for the Natural Numbers *}
    1.11  
    1.12 -instance nat :: recpower ..
    1.13 -
    1.14  lemma nat_one_le_power [simp]:
    1.15    "Suc 0 \<le> i \<Longrightarrow> Suc 0 \<le> i ^ n"
    1.16    by (rule one_le_power [of i n, unfolded One_nat_def])