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}