doc-src/TutorialI/CTL/PDL.thy

 \ \isadigit{1}{\isachardot}\ {\isasymAnd}t{\isachardot}\ t\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}
 \end{isabelle}
 is solved by unrolling @{term lfp} once
 *}
 
- apply(rule ssubst[OF lfp_Tarski[OF mono_ef]])
+ apply(rule ssubst[OF lfp_unfold[OF mono_ef]])
 (*pr(latex xsymbols symbols);*)
 txt{*
 \begin{isabelle}
 \ \isadigit{1}{\isachardot}\ {\isasymAnd}t{\isachardot}\ t\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}
 \end{isabelle}

 
 txt{*\noindent
 The proof of the induction step is identical to the one for the base case:
 *}
 
-apply(rule ssubst[OF lfp_Tarski[OF mono_ef]])
+apply(rule ssubst[OF lfp_unfold[OF mono_ef]])
 apply(blast)
 done
 
 text{*
 The main theorem is proved in the familiar manner: induction followed by

 done;
 
 lemma "(s \<Turnstile> EF f) = (s \<Turnstile> f | s \<Turnstile> Neg(AX(Neg(EF f))))";
 apply(simp only:aux);
 apply(simp);
-apply(rule ssubst[OF lfp_Tarski[OF mono_ef]], fast);
+apply(rule ssubst[OF lfp_unfold[OF mono_ef]], fast);
 done
 
 end
 (*>*)