diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/CTL/document/Base.tex
--- a/doc-src/TutorialI/CTL/document/Base.tex	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/Base.tex	Fri Jan 05 18:32:57 2001 +0100
@@ -8,9 +8,9 @@
 \begin{isamarkuptext}%
 \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 (\isa{{\isasymTurnstile}}) and a