
diff -r fb9be005cc44 -r 194c7349b6c0 doc-src/TutorialI/CTL/PDL.thy
--- 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




