--- a/doc-src/TutorialI/CTL/Base.thy Mon Oct 09 17:40:47 2000 +0200
+++ b/doc-src/TutorialI/CTL/Base.thy Mon Oct 09 19:20:55 2000 +0200
@@ -7,7 +7,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 (@{text \<Turnstile>}) and a
recursive function @{term mc} that maps a formula into the set of all states of