src/HOL/Relation_Power.thy

--- a/src/HOL/Relation_Power.thy	Thu May 17 11:31:21 2001 +0200
+++ b/src/HOL/Relation_Power.thy	Fri May 18 07:56:19 2001 +0200
@@ -4,6 +4,7 @@
     Copyright   1996  TU Muenchen
 
 R^n = R O ... O R, the n-fold composition of R
+Both for functions and relations.
 *)
 
 Relation_Power = Nat +
@@ -15,4 +16,11 @@
   "R^0 = Id"
   "R^(Suc n) = R O (R^n)"
 
+
+instance fun :: (term,term)power   (* only 'a \<Rightarrow> 'a should be in power! *)
+
+primrec (funpow)
+  "f^0 = id"
+  "f^(Suc n) = f o (f^n)"
+
 end