diff -r 383b0a1837a9 -r aecb5bf6f76f doc-src/TutorialI/CTL/document/Base.tex
--- a/doc-src/TutorialI/CTL/document/Base.tex	Mon Oct 09 17:40:47 2000 +0200
+++ b/doc-src/TutorialI/CTL/document/Base.tex	Mon Oct 09 19:20:55 2000 +0200
@@ -9,7 +9,7 @@
 state systems (implementations) w.r.t.\ temporal logic formulae
 (specifications) \cite{Clark}. Its foundations are completely set theoretic
 and this section shall develop them in HOL. This is done in two steps: first
-we consider a very simple ``temporal'' logic called propositional dynamic
+we consider a simple modal logic called propositional dynamic
 logic (PDL) which we then extend to the temporal logic CTL used in many real
 model checkers. In each case we give both a traditional semantics (\isa{{\isasymTurnstile}}) and a
 recursive function \isa{mc} that maps a formula into the set of all states of