*** empty log message ***
authornipkow
Mon, 02 Oct 2000 14:25:10 +0200
changeset 10122 194c7349b6c0
parent 10121 fb9be005cc44
child 10123 9469c039ff57
*** empty log message ***
doc-src/TutorialI/CTL/PDL.thy
doc-src/TutorialI/IsaMakefile
--- 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
--- a/doc-src/TutorialI/IsaMakefile	Mon Oct 02 14:22:39 2000 +0200
+++ b/doc-src/TutorialI/IsaMakefile	Mon Oct 02 14:25:10 2000 +0200
@@ -106,7 +106,7 @@
 
 HOL-CTL: HOL $(LOG)/HOL-CTL.gz
 
-$(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/PDL.thy CTL/CTL.thy CTL/ROOT.ML
+$(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/ROOT.ML
 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL CTL
 	@rm -f tutorial.dvi