src/HOL/Transitive_Closure.thy

   assumes major: "r\<^sup>*\<^sup>* x z"
     and cases: "x = z \<Longrightarrow> P" "\<And>y. r x y \<Longrightarrow> r\<^sup>*\<^sup>* y z \<Longrightarrow> P"
   shows P
 proof -
   have "x = z \<or> (\<exists>y. r x y \<and> r\<^sup>*\<^sup>* y z)"
-    by (rule_tac major [THEN converse_rtranclp_induct]) iprover+
+    by (rule major [THEN converse_rtranclp_induct]) iprover+
   then show ?thesis
     by (auto intro: cases)
 qed
 
 lemmas converse_rtranclE = converse_rtranclpE [to_set]

   case 0
   show ?case by auto
 next
   case (Suc n)
   show ?case
-  proof (simp add: relcomp_unfold Suc)
-    show "(\<exists>y. (\<exists>f. f 0 = a \<and> f n = y \<and> (\<forall>i<n. (f i,f(Suc i)) \<in> R)) \<and> (y,b) \<in> R) \<longleftrightarrow>
+  proof -
+    have "(\<exists>y. (\<exists>f. f 0 = a \<and> f n = y \<and> (\<forall>i<n. (f i,f(Suc i)) \<in> R)) \<and> (y,b) \<in> R) \<longleftrightarrow>
       (\<exists>f. f 0 = a \<and> f(Suc n) = b \<and> (\<forall>i<Suc n. (f i, f (Suc i)) \<in> R))"
-    (is "?l = ?r")
+      (is "?l \<longleftrightarrow> ?r")
     proof
       assume ?l
       then obtain c f
         where 1: "f 0 = a"  "f n = c"  "\<And>i. i < n \<Longrightarrow> (f i, f (Suc i)) \<in> R"  "(c,b) \<in> R"
         by auto

       show ?r by (rule exI[of _ ?g]) (simp add: 1)
     next
       assume ?r
       then obtain f where 1: "f 0 = a"  "b = f (Suc n)"  "\<And>i. i < Suc n \<Longrightarrow> (f i, f (Suc i)) \<in> R"
         by auto
-      show ?l by (rule exI[of _ "f n"], rule conjI, rule exI[of _ f], insert 1, auto)
+      show ?l by (rule exI[of _ "f n"], rule conjI, rule exI[of _ f], auto simp add: 1)
     qed
+    then show ?thesis by (simp add: relcomp_unfold Suc)
   qed
 qed
 
 lemma relpowp_fun_conv: "(P ^^ n) x y \<longleftrightarrow> (\<exists>f. f 0 = x \<and> f n = y \<and> (\<forall>i<n. P (f i) (f (Suc i))))"
   by (fact relpow_fun_conv [to_pred])