| changeset 10122 | 194c7349b6c0 |
| parent 9958 | 67f2920862c7 |
| child 10133 | e187dacd248f |
--- a/doc-src/TutorialI/CTL/PDL.thy Mon Oct 02 14:22:39 2000 +0200 +++ b/doc-src/TutorialI/CTL/PDL.thy Mon Oct 02 14:25:10 2000 +0200 @@ -1,7 +1,6 @@ -theory PDL = Main:; +(*<*)theory PDL = Base:(*>*) -typedecl atom; -types state = "atom set"; +subsection{*Propositional dynmic logic---PDL*} datatype ctl_form = Atom atom | NOT ctl_form