1.1 --- a/doc-src/TutorialI/CTL/PDL.thy	Wed Jan 24 11:59:15 2001 +0100
     1.2 +++ b/doc-src/TutorialI/CTL/PDL.thy	Wed Jan 24 12:29:10 2001 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4  (*<*)theory PDL = Base:(*>*)
     1.5  
     1.6 -subsection{*Propositional Dynamic Logic---PDL*}
     1.7 +subsection{*Propositional Dynamic Logic --- PDL*}
     1.8  
     1.9  text{*\index{PDL|(}
    1.10  The formulae of PDL are built up from atomic propositions via the customary
    1.11 @@ -68,7 +68,7 @@
    1.12  fixed point (@{term lfp}) of @{term"\<lambda>T. mc f \<union> M\<inverse> `` T"} is the least set
    1.13  @{term T} containing @{term"mc f"} and all predecessors of @{term T}. If you
    1.14  find it hard to see that @{term"mc(EF f)"} contains exactly those states from
    1.15 -which there is a path to a state where @{term f} is true, do not worry---that
    1.16 +which there is a path to a state where @{term f} is true, do not worry --- that
    1.17  will be proved in a moment.
    1.18  
    1.19  First we prove monotonicity of the function inside @{term lfp}