--- a/src/HOL/Transitive_Closure.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Transitive_Closure.thy Wed Feb 12 08:37:06 2014 +0100
@@ -846,6 +846,7 @@
\<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ m \<Longrightarrow> P)
\<Longrightarrow> P"
apply (cases n, simp)
+ apply (rename_tac nat)
apply (cut_tac n=nat and R=R in relpow_Suc_D2', simp, blast)
done
@@ -1297,4 +1298,3 @@
{* simple transitivity reasoner (predicate version) *}
end
-