changeset 17914 | 99ead7a7eb42 |
parent 12815 | 1f073030b97a |
child 18724 | cb6e0064c88c |
17913:4159e1523ad8 | 17914:99ead7a7eb42 |
---|---|
1 (*<*)theory PDL = Base:(*>*) |
1 (*<*)theory PDL imports Base begin(*>*) |
2 |
2 |
3 subsection{*Propositional Dynamic Logic --- PDL*} |
3 subsection{*Propositional Dynamic Logic --- PDL*} |
4 |
4 |
5 text{*\index{PDL|(} |
5 text{*\index{PDL|(} |
6 The formulae of PDL are built up from atomic propositions via |
6 The formulae of PDL are built up from atomic propositions via |