diff -r 2ce86fccc95b -r 6f4ed75b2dca src/HOL/Relation_Power.thy
--- a/src/HOL/Relation_Power.thy	Fri May 18 07:56:19 2001 +0200
+++ b/src/HOL/Relation_Power.thy	Fri May 18 12:09:13 2001 +0200
@@ -4,7 +4,12 @@
     Copyright   1996  TU Muenchen
 
 R^n = R O ... O R, the n-fold composition of R
-Both for functions and relations.
+f^n = f o ... o f, the n-fold composition of f
+
+WARNING: due to the limits of Isabelle's type classes, ^ on functions and
+relations has too general a domain, namely ('a * 'b)set and 'a => 'b.
+This means that it may be necessary to attach explicit type constraints.
+Examples: range(f^n) = A and Range(R^n) = B need constraints.
 *)
 
 Relation_Power = Nat +
@@ -17,7 +22,8 @@
   "R^(Suc n) = R O (R^n)"
 
 
-instance fun :: (term,term)power   (* only 'a \<Rightarrow> 'a should be in power! *)
+instance
+  fun :: (term,term)power   (* only 'a => 'a should be in power! *)
 
 primrec (funpow)
   "f^0 = id"