1.1 --- a/doc-src/TutorialI/CTL/PDL.thy Mon Oct 02 14:22:39 2000 +0200
1.2 +++ b/doc-src/TutorialI/CTL/PDL.thy Mon Oct 02 14:25:10 2000 +0200
1.3 @@ -1,7 +1,6 @@
1.4 -theory PDL = Main:;
1.5 +(*<*)theory PDL = Base:(*>*)
1.6
1.7 -typedecl atom;
1.8 -types state = "atom set";
1.9 +subsection{*Propositional dynmic logic---PDL*}
1.10
1.11 datatype ctl_form = Atom atom
1.12 | NOT ctl_form
2.1 --- a/doc-src/TutorialI/IsaMakefile Mon Oct 02 14:22:39 2000 +0200
2.2 +++ b/doc-src/TutorialI/IsaMakefile Mon Oct 02 14:25:10 2000 +0200
2.3 @@ -106,7 +106,7 @@
2.4
2.5 HOL-CTL: HOL $(LOG)/HOL-CTL.gz
2.6
2.7 -$(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/PDL.thy CTL/CTL.thy CTL/ROOT.ML
2.8 +$(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/ROOT.ML
2.9 @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL CTL
2.10 @rm -f tutorial.dvi
2.11