added comments
authornipkow
Fri May 18 12:09:13 2001 +0200 (2001-05-18)
changeset 113066f4ed75b2dca
parent 11305 2ce86fccc95b
child 11307 891fbd3f4881
added comments
src/HOL/Relation_Power.thy
     1.1 --- a/src/HOL/Relation_Power.thy	Fri May 18 07:56:19 2001 +0200
     1.2 +++ b/src/HOL/Relation_Power.thy	Fri May 18 12:09:13 2001 +0200
     1.3 @@ -4,7 +4,12 @@
     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 +f^n = f o ... o f, the n-fold composition of f
     1.9 +
    1.10 +WARNING: due to the limits of Isabelle's type classes, ^ on functions and
    1.11 +relations has too general a domain, namely ('a * 'b)set and 'a => 'b.
    1.12 +This means that it may be necessary to attach explicit type constraints.
    1.13 +Examples: range(f^n) = A and Range(R^n) = B need constraints.
    1.14  *)
    1.15  
    1.16  Relation_Power = Nat +
    1.17 @@ -17,7 +22,8 @@
    1.18    "R^(Suc n) = R O (R^n)"
    1.19  
    1.20  
    1.21 -instance fun :: (term,term)power   (* only 'a \<Rightarrow> 'a should be in power! *)
    1.22 +instance
    1.23 +  fun :: (term,term)power   (* only 'a => 'a should be in power! *)
    1.24  
    1.25  primrec (funpow)
    1.26    "f^0 = id"