diff -r cf8956f49499 -r bda1701848cd doc-src/TutorialI/CTL/document/Base.tex
--- a/doc-src/TutorialI/CTL/document/Base.tex	Thu Jan 11 11:47:57 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/Base.tex	Thu Jan 11 12:12:01 2001 +0100
@@ -2,22 +2,25 @@
 \begin{isabellebody}%
 \def\isabellecontext{Base}%
 %
-\isamarkupsection{Case study: Verified model checking%
+\isamarkupsection{Case Study: Verified Model Checking%
 }
 %
 \begin{isamarkuptext}%
 \label{sec:VMC}
-Model checking is a very popular technique for the verification of finite
+This chapter ends with a case study concerning model checking for 
+Computation Tree Logic (CTL), a temporal logic.
+Model checking is a popular technique for the verification of finite
 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 will explore them a little in HOL\@. This is done in two steps: first
+(specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are set theoretic
+and this section will explore them 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
+logic (PDL), which we then extend to the temporal logic CTL, which is
+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
 the system where the formula is valid. If the system has a finite number of
-states, \isa{mc} is directly executable, i.e.\ a model checker, albeit not a
-very efficient one. The main proof obligation is to show that the semantics
+states, \isa{mc} is directly executable: it is a model checker, albeit an
+inefficient one. The main proof obligation is to show that the semantics
 and the model checker agree.
 
 \underscoreon
@@ -66,7 +69,7 @@
 course it would have been more generic to make \isa{state} a type
 parameter of everything but declaring \isa{state} globally as above
 reduces clutter.  Similarly we declare an arbitrary but fixed
-transition system, i.e.\ relation between states:%
+transition system, i.e.\ a relation between states:%
 \end{isamarkuptext}%
 \isacommand{consts}\ M\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}state\ {\isasymtimes}\ state{\isacharparenright}set{\isachardoublequote}%
 \begin{isamarkuptext}%