# HG changeset patch
# User nipkow
# Date 990165379 -7200
# Node ID 2ce86fccc95b7f95204ad6ac6cb98151948b59bd
# Parent  0db2a02bff99c675f91ff23d384d0b738c07ef62
added ^ on functions.

diff -r 0db2a02bff99 -r 2ce86fccc95b 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