summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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}