--- a/src/HOL/Power.thy Tue May 09 14:16:32 2000 +0200
+++ b/src/HOL/Power.thy Tue May 09 14:33:43 2000 +0200
@@ -11,7 +11,7 @@
consts
binomial :: "[nat,nat] => nat" (infixl "choose" 65)
-primrec
+primrec (power)
"p ^ 0 = 1"
"p ^ (Suc n) = (p::nat) * (p ^ n)"