doc-src/TutorialI/CTL/PDL.thy
 changeset 10971 6852682eaf16 parent 10895 79194f07d356 child 10983 59961d32b1ae
```     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}
```