--- a/doc-src/TutorialI/CTL/PDL.thy Wed Oct 11 00:03:22 2000 +0200
+++ b/doc-src/TutorialI/CTL/PDL.thy Wed Oct 11 09:09:06 2000 +0200
@@ -158,7 +158,7 @@
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}
@@ -173,7 +173,7 @@
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
@@ -213,7 +213,7 @@
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