doc-src/TutorialI/CTL/document/PDL.tex
changeset 10212 33fe2d701ddd
parent 10211 1bece7f35762
child 10242 028f54cd2cc9
     1.1 --- a/doc-src/TutorialI/CTL/document/PDL.tex	Thu Oct 12 18:09:06 2000 +0200
     1.2 +++ b/doc-src/TutorialI/CTL/document/PDL.tex	Thu Oct 12 18:38:23 2000 +0200
     1.3 @@ -113,10 +113,9 @@
     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 \isa{blast} with the help of a few lemmas about
     1.8 -\isa{{\isacharcircum}{\isacharasterisk}}:%
     1.9 +which is proved by \isa{blast} with the help of transitivity of \isa{{\isacharcircum}{\isacharasterisk}}:%
    1.10  \end{isamarkuptxt}%
    1.11 -\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ r{\isacharunderscore}into{\isacharunderscore}rtrancl\ rtrancl{\isacharunderscore}trans{\isacharparenright}%
    1.12 +\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtrancl{\isacharunderscore}trans{\isacharparenright}%
    1.13  \begin{isamarkuptxt}%
    1.14  We now return to the second set containment subgoal, which is again proved
    1.15  pointwise:%