diff -r 279da0358aa9 -r 09a6c44a48ea doc-src/TutorialI/CTL/document/PDL.tex
--- a/doc-src/TutorialI/CTL/document/PDL.tex	Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/CTL/document/PDL.tex	Fri Aug 03 18:04:55 2001 +0200
@@ -7,12 +7,13 @@
 %
 \begin{isamarkuptext}%
 \index{PDL|(}
-The formulae of PDL\footnote{The customary definition of PDL
+The formulae of PDL are built up from atomic propositions via
+negation and conjunction and the two temporal
+connectives \isa{AX} and \isa{EF}\@. Since formulae are essentially
+syntax trees, they are naturally modelled as a datatype:%
+\footnote{The customary definition of PDL
 \cite{HarelKT-DL} looks quite different from ours, but the two are easily
-shown to be equivalent.} are built up from atomic propositions via
-negation and conjunction and the two temporal
-connectives \isa{AX} and \isa{EF}. Since formulae are essentially
-syntax trees, they are naturally modelled as a datatype:%
+shown to be equivalent.}%
 \end{isamarkuptext}%
 \isacommand{datatype}\ formula\ {\isacharequal}\ Atom\ atom\isanewline
 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Neg\ formula\isanewline
@@ -21,19 +22,16 @@
 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ EF\ formula%
 \begin{isamarkuptext}%
 \noindent
-This is almost the same as in the boolean expression case study in
+This resembles the boolean expression case study in
 \S\ref{sec:boolex}.
-
-The meaning of these formulae is given by saying which formula is true in
-which state:%
+A validity relation between
+states and formulae specifies the semantics:%
 \end{isamarkuptext}%
 \isacommand{consts}\ valid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ formula\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharparenleft}{\isacharunderscore}\ {\isasymTurnstile}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{8}}{\isadigit{0}}{\isacharcomma}{\isadigit{8}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{8}}{\isadigit{0}}{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
 The syntax annotation allows us to write \isa{s\ {\isasymTurnstile}\ f} instead of
 \hbox{\isa{valid\ s\ f}}.
-
-\smallskip
 The definition of \isa{{\isasymTurnstile}} is by recursion over the syntax:%
 \end{isamarkuptext}%
 \isacommand{primrec}\isanewline
@@ -51,8 +49,7 @@
 closure. Because of reflexivity, the future includes the present.
 
 Now we come to the model checker itself. It maps a formula into the set of
-states where the formula is true and is defined by recursion over the syntax,
-too:%
+states where the formula is true.  It too is defined by recursion over the syntax:%
 \end{isamarkuptext}%
 \isacommand{consts}\ mc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}formula\ {\isasymRightarrow}\ state\ set{\isachardoublequote}\isanewline
 \isacommand{primrec}\isanewline
@@ -109,13 +106,14 @@
 \begin{isamarkuptxt}%
 \noindent
 Having disposed of the monotonicity subgoal,
-simplification leaves us with the following main goal
+simplification leaves us with the following goal:
 \begin{isabelle}
 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymor}\isanewline
 \ \ \ \ \ \ \ \ \ x\ {\isasymin}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ {\isacharparenleft}lfp\ {\isacharparenleft}\dots{\isacharparenright}\ {\isasyminter}\ {\isacharbraceleft}x{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isacharparenright}\isanewline
 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A
 \end{isabelle}
-which is proved by \isa{blast} with the help of transitivity of \isa{\isactrlsup {\isacharasterisk}}:%
+It is proved by \isa{blast}, using the transitivity of 
+\isa{M\isactrlsup {\isacharasterisk}}.%
 \end{isamarkuptxt}%
 \ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtrancl{\isacharunderscore}trans{\isacharparenright}%
 \begin{isamarkuptxt}%
@@ -132,7 +130,7 @@
 \end{isabelle}
 This goal is proved by induction on \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}}. But since the model
 checker works backwards (from \isa{t} to \isa{s}), we cannot use the
-induction theorem \isa{rtrancl{\isacharunderscore}induct} because it works in the
+induction theorem \isa{rtrancl{\isacharunderscore}induct}: it works in the
 forward direction. Fortunately the converse induction theorem
 \isa{converse{\isacharunderscore}rtrancl{\isacharunderscore}induct} already exists:
 \begin{isabelle}%
@@ -178,9 +176,11 @@
 \isacommand{done}%
 \begin{isamarkuptext}%
 \begin{exercise}
-\isa{AX} has a dual operator \isa{EN}\footnote{We cannot use the customary \isa{EX}
-as that is the \textsc{ascii}-equivalent of \isa{{\isasymexists}}}
-(``there exists a next state such that'') with the intended semantics
+\isa{AX} has a dual operator \isa{EN} 
+(``there exists a next state such that'')%
+\footnote{We cannot use the customary \isa{EX}: it is reserved
+as the \textsc{ascii}-equivalent of \isa{{\isasymexists}}.}
+with the intended semantics
 \begin{isabelle}%
 \ \ \ \ \ s\ {\isasymTurnstile}\ EN\ f\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymTurnstile}\ f{\isacharparenright}%
 \end{isabelle}