doc-src/TutorialI/CTL/PDL.thy

 @{text auto} augmented with the lemma as a simplification rule.
 *}
 
 theorem "mc f = {s. s \<Turnstile> f}"
 apply(induct_tac f)
-apply(auto simp add:EF_lemma)
+apply(auto simp add: EF_lemma)
 done
 
 text{*
 \begin{exercise}
 @{term AX} has a dual operator @{term EN}