--- a/doc-src/TutorialI/CTL/document/PDL.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/PDL.tex Wed Jan 24 12:29:10 2001 +0100
@@ -2,7 +2,7 @@
\begin{isabellebody}%
\def\isabellecontext{PDL}%
%
-\isamarkupsubsection{Propositional Dynamic Logic---PDL%
+\isamarkupsubsection{Propositional Dynamic Logic --- PDL%
}
%
\begin{isamarkuptext}%
@@ -68,7 +68,7 @@
fixed point (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T} is the least set
\isa{T} containing \isa{mc\ f} and all predecessors of \isa{T}. If you
find it hard to see that \isa{mc\ {\isacharparenleft}EF\ f{\isacharparenright}} contains exactly those states from
-which there is a path to a state where \isa{f} is true, do not worry---that
+which there is a path to a state where \isa{f} is true, do not worry --- that
will be proved in a moment.
First we prove monotonicity of the function inside \isa{lfp}