merged

--- a/src/HOL/Transitive_Closure.thy	Mon Jun 01 07:57:37 2009 -0700
+++ b/src/HOL/Transitive_Closure.thy	Mon Jun 01 08:04:19 2009 -0700
@@ -698,6 +698,9 @@
   apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast)
   done
 
+lemma rel_pow_add: "R ^^ (m+n) = R^^n O R^^m"
+by(induct n) auto
+
 lemma rtrancl_imp_UN_rel_pow:
   assumes "p \<in> R^*"
   shows "p \<in> (\<Union>n. R ^^ n)"