doc-src/TutorialI/CTL/PDL.thy
 changeset 10212 33fe2d701ddd parent 10210 e8aa81362f41 child 10242 028f54cd2cc9
     1.1 --- a/doc-src/TutorialI/CTL/PDL.thy	Thu Oct 12 18:09:06 2000 +0200
1.2 +++ b/doc-src/TutorialI/CTL/PDL.thy	Thu Oct 12 18:38:23 2000 +0200
1.3 @@ -118,11 +118,10 @@
1.4  \ \ \ \ \ \ \ \ \ s\ {\isasymin}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ {\isacharparenleft}lfp\ {\isacharparenleft}{\dots}{\isacharparenright}\ {\isasyminter}\ {\isacharbraceleft}x{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isacharparenright}\isanewline
1.5  \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A
1.6  \end{isabelle}
1.7 -which is proved by @{text blast} with the help of a few lemmas about
1.8 -@{text"^*"}:
1.9 +which is proved by @{text blast} with the help of transitivity of @{text"^*"}:
1.10  *}
1.11
1.12 - apply(blast intro: r_into_rtrancl rtrancl_trans);
1.13 + apply(blast intro: rtrancl_trans);
1.14
1.15  txt{*
1.16  We now return to the second set containment subgoal, which is again proved