doc-src/TutorialI/CTL/document/PDL.tex
changeset 10971 6852682eaf16
parent 10950 aa788fcb75a5
child 10983 59961d32b1ae
     1.1 --- a/doc-src/TutorialI/CTL/document/PDL.tex	Wed Jan 24 11:59:15 2001 +0100
     1.2 +++ b/doc-src/TutorialI/CTL/document/PDL.tex	Wed Jan 24 12:29:10 2001 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4  \begin{isabellebody}%
     1.5  \def\isabellecontext{PDL}%
     1.6  %
     1.7 -\isamarkupsubsection{Propositional Dynamic Logic---PDL%
     1.8 +\isamarkupsubsection{Propositional Dynamic Logic --- PDL%
     1.9  }
    1.10  %
    1.11  \begin{isamarkuptext}%
    1.12 @@ -68,7 +68,7 @@
    1.13  fixed point (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T} is the least set
    1.14  \isa{T} containing \isa{mc\ f} and all predecessors of \isa{T}. If you
    1.15  find it hard to see that \isa{mc\ {\isacharparenleft}EF\ f{\isacharparenright}} contains exactly those states from
    1.16 -which there is a path to a state where \isa{f} is true, do not worry---that
    1.17 +which there is a path to a state where \isa{f} is true, do not worry --- that
    1.18  will be proved in a moment.
    1.19  
    1.20  First we prove monotonicity of the function inside \isa{lfp}