1.1 --- a/src/HOL/Relation_Power.thy	Thu May 17 11:31:21 2001 +0200
     1.2 +++ b/src/HOL/Relation_Power.thy	Fri May 18 07:56:19 2001 +0200
     1.3 @@ -4,6 +4,7 @@
     1.4      Copyright   1996  TU Muenchen
     1.5  
     1.6  R^n = R O ... O R, the n-fold composition of R
     1.7 +Both for functions and relations.
     1.8  *)
     1.9  
    1.10  Relation_Power = Nat +
    1.11 @@ -15,4 +16,11 @@
    1.12    "R^0 = Id"
    1.13    "R^(Suc n) = R O (R^n)"
    1.14  
    1.15 +
    1.16 +instance fun :: (term,term)power   (* only 'a \<Rightarrow> 'a should be in power! *)
    1.17 +
    1.18 +primrec (funpow)
    1.19 +  "f^0 = id"
    1.20 +  "f^(Suc n) = f o (f^n)"
    1.21 +
    1.22  end