src/HOL/Power.thy
changeset 21456 1c2b9df41e98
parent 21413 0951647209f2
child 22390 378f34b1e380
     1.1 --- a/src/HOL/Power.thy	Wed Nov 22 10:20:15 2006 +0100
     1.2 +++ b/src/HOL/Power.thy	Wed Nov 22 10:20:16 2006 +0100
     1.3 @@ -311,6 +311,8 @@
     1.4  
     1.5  subsection{*Exponentiation for the Natural Numbers*}
     1.6  
     1.7 +instance nat :: power ..
     1.8 +
     1.9  primrec (power)
    1.10    "p ^ 0 = 1"
    1.11    "p ^ (Suc n) = (p::nat) * (p ^ n)"