doc-src/TutorialI/CTL/CTLind.thy

 into a @{text"\<And>p"}, which would complicate matters below. As it is,
 @{thm[source]Avoid_in_lfp} is now
 @{thm[display]Avoid_in_lfp[no_vars]}
 The main theorem is simply the corollary where @{prop"t = s"},
 in which case the assumption @{prop"t \<in> Avoid s A"} is trivially true
-by the first @{term Avoid}-rule). Isabelle confirms this:
+by the first @{term Avoid}-rule. Isabelle confirms this:
 *}
 
 theorem AF_lemma2:
   "{s. \<forall>p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
 by(auto elim:Avoid_in_lfp intro:Avoid.intros);