--- a/doc-src/TutorialI/CTL/Base.thy Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/CTL/Base.thy Fri Jan 05 18:32:57 2001 +0100
@@ -4,9 +4,9 @@
text{*\label{sec:VMC}
Model checking is a very popular technique for the verification of finite
-state systems (implementations) w.r.t.\ temporal logic formulae
+state systems (implementations) with respect to temporal logic formulae
(specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic
-and this section shall explore them a little in HOL. This is done in two steps: first
+and this section will explore them a little in HOL\@. This is done in two steps: first
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