--- a/src/HOL/Hoare/SchorrWaite.thy Tue Mar 29 21:48:01 2011 +0200
+++ b/src/HOL/Hoare/SchorrWaite.thy Tue Mar 29 22:36:56 2011 +0200
@@ -40,7 +40,7 @@
done
lemma still_reachable: "\<lbrakk>B\<subseteq>Ra\<^sup>*``A; \<forall> (x,y) \<in> Rb-Ra. y\<in> (Ra\<^sup>*``A)\<rbrakk> \<Longrightarrow> Rb\<^sup>* `` B \<subseteq> Ra\<^sup>* `` A "
-apply (clarsimp simp only:Image_iff intro:subsetI)
+apply (clarsimp simp only:Image_iff)
apply (erule rtrancl_induct)
apply blast
apply (subgoal_tac "(y, z) \<in> Ra\<union>(Rb-Ra)")