--- a/src/HOL/Transitive_Closure.thy Mon Jan 30 13:55:22 2012 +0100
+++ b/src/HOL/Transitive_Closure.thy Mon Jan 30 13:55:23 2012 +0100
@@ -718,6 +718,18 @@
end
+text {* for code generation *}
+
+definition relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where
+ relpow_code_def [code_abbrev]: "relpow = compow"
+
+lemma [code]:
+ "relpow (Suc n) R = (relpow n R) O R"
+ "relpow 0 R = Id"
+ by (simp_all add: relpow_code_def)
+
+hide_const (open) relpow
+
lemma rel_pow_1 [simp]:
fixes R :: "('a \<times> 'a) set"
shows "R ^^ 1 = R"