named "op ^" definitions;

--- 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)"
   

--- a/src/HOL/RelPow.thy	Tue May 09 14:16:32 2000 +0200
+++ b/src/HOL/RelPow.thy	Tue May 09 14:33:43 2000 +0200
@@ -11,7 +11,7 @@
 instance
   set :: (term) {power}   (* only ('a * 'a) set should be in power! *)
 
-primrec
+primrec (relpow)
   "R^0 = Id"
   "R^(Suc n) = R O (R^n)"