src/HOL/Transitive_Closure.thy

   -- {* primitive recursion for @{text trancl} over finite relations *}
   apply (rule equalityI)
    apply (rule subsetI)
    apply (simp only: split_tupled_all)
    apply (erule trancl_induct, blast)
-   apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl r_into_trancl trancl_trans)
+   apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl trancl_trans)
   apply (rule subsetI)
   apply (blast intro: trancl_mono rtrancl_mono
     [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2)
   done
 

       "!!y z.[| r y z;  r^++ z b;  P(z) |] ==> P(y)"
   shows "P a"
   apply (rule tranclp_induct [OF tranclp_converseI, OF conversepI, OF major])
    apply (rule cases)
    apply (erule conversepD)
-  apply (blast intro: prems dest!: tranclp_converseD conversepD)
+  apply (blast intro: assms dest!: tranclp_converseD)
   done
 
 lemmas converse_trancl_induct = converse_tranclp_induct [to_set]
 
 lemma tranclpD: "R^++ x y ==> EX z. R x z \<and> R^** z y"