primrec definition for ^

--- a/src/HOL/RelPow.thy	Thu Mar 06 16:05:32 1997 +0100
+++ b/src/HOL/RelPow.thy	Thu Mar 06 16:06:08 1997 +0100
@@ -10,6 +10,9 @@
 
 consts
   "^" :: "('a * 'a) set => nat => ('a * 'a) set" (infixr 100)
-defs
-  rel_pow_def "R^n == nat_rec id (%m S. R O S) n"
+
+primrec "op ^" nat
+  "R^0 = id"
+  "R^(Suc n) = R O (R^n)"
+
 end