--- a/src/HOL/Power.thy Wed Nov 22 10:20:15 2006 +0100
+++ b/src/HOL/Power.thy Wed Nov 22 10:20:16 2006 +0100
@@ -311,6 +311,8 @@
subsection{*Exponentiation for the Natural Numbers*}
+instance nat :: power ..
+
primrec (power)
"p ^ 0 = 1"
"p ^ (Suc n) = (p::nat) * (p ^ n)"