diff -r 06e6f352df1b -r 69cee87927f0 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Fri Mar 30 00:01:30 2012 +0100
+++ b/src/HOL/Transitive_Closure.thy	Fri Mar 30 09:04:29 2012 +0200
@@ -710,14 +710,24 @@
 
 overloading
   relpow == "compow :: nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"
+  relpowp == "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"
 begin
 
 primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where
     "relpow 0 R = Id"
   | "relpow (Suc n) R = (R ^^ n) O R"
 
+primrec relpowp :: "nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" where
+    "relpowp 0 R = HOL.eq"
+  | "relpowp (Suc n) R = (R ^^ n) OO R"
+
 end
 
+lemma relpowp_relpow_eq [pred_set_conv]:
+  fixes R :: "'a rel"
+  shows "(\<lambda>x y. (x, y) \<in> R) ^^ n = (\<lambda>x y. (x, y) \<in> R ^^ n)"
+  by (induct n) (simp_all add: rel_compp_rel_comp_eq)
+
 text {* for code generation *}
 
 definition relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where