# HG changeset patch
# User wenzelm
# Date 957875623 -7200
# Node ID db71c334e854ed6cabbaddd8fd768787bd080dc2
# Parent  5370a030dd471521e046828a411a7e01a3073837
named "op ^" definitions;

diff -r 5370a030dd47 -r db71c334e854 src/HOL/Power.thy
--- 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)"
   
diff -r 5370a030dd47 -r db71c334e854 src/HOL/RelPow.thy
--- 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)"