diff -r c452fea3ce74 -r 499637e8f2c6 doc-src/TutorialI/CTL/document/Base.tex
--- a/doc-src/TutorialI/CTL/document/Base.tex	Wed Oct 11 00:03:22 2000 +0200
+++ b/doc-src/TutorialI/CTL/document/Base.tex	Wed Oct 11 09:09:06 2000 +0200
@@ -2,13 +2,13 @@
 \begin{isabellebody}%
 \def\isabellecontext{Base}%
 %
-\isamarkupsection{A verified model checker}
+\isamarkupsection{Case study: Verified model checkers}
 %
 \begin{isamarkuptext}%
 Model checking is a very popular technique for the verification of finite
 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
+(specifications) \cite{Clarke,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
 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
@@ -47,8 +47,9 @@
 Each state has a unique name or number ($s_0,s_1,s_2$), and in each
 state certain \emph{atomic propositions} ($p,q,r$) are true.
 The aim of temporal logic is to formalize statements such as ``there is no
-transition sequence starting from $s_2$ leading to a state where $p$ or $q$
-are true''.
+path starting from $s_2$ leading to a state where $p$ or $q$
+are true'', which is true, and ``on all paths starting from $s_0$ $q$ is always true'',
+which is false.
 
 Abstracting from this concrete example, we assume there is some type of
 states%