--- a/src/HOL/Transitive_Closure.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/Transitive_Closure.thy Thu Aug 27 21:19:48 2015 +0200
@@ -169,8 +169,9 @@
lemma rtrancl_Int_subset: "[| Id \<subseteq> s; (r^* \<inter> s) O r \<subseteq> s|] ==> r^* \<subseteq> s"
apply (rule subsetI)
- apply (rule_tac p="x" in PairE, clarify)
- apply (erule rtrancl_induct, auto)
+ apply auto
+ apply (erule rtrancl_induct)
+ apply auto
done
lemma converse_rtranclp_into_rtranclp:
@@ -409,10 +410,9 @@
lemma trancl_Int_subset: "[| r \<subseteq> s; (r^+ \<inter> s) O r \<subseteq> s|] ==> r^+ \<subseteq> s"
apply (rule subsetI)
- apply (rule_tac p = x in PairE)
- apply clarify
+ apply auto
apply (erule trancl_induct)
- apply auto
+ apply auto
done
lemma trancl_unfold: "r^+ = r Un r^+ O r"