diff -r 55c0f9a8df78 -r 59961d32b1ae doc-src/TutorialI/CTL/PDL.thy
--- a/doc-src/TutorialI/CTL/PDL.thy	Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/CTL/PDL.thy	Fri Jan 26 15:50:28 2001 +0100
@@ -42,8 +42,8 @@
 
 text{*\noindent
 The first three equations should be self-explanatory. The temporal formula
-@{term"AX f"} means that @{term f} is true in all next states whereas
-@{term"EF f"} means that there exists some future state in which @{term f} is
+@{term"AX f"} means that @{term f} is true in \emph{A}ll ne\emph{X}t states whereas
+@{term"EF f"} means that there \emph{E}xists some \emph{F}uture state in which @{term f} is
 true. The future is expressed via @{text"\<^sup>*"}, the reflexive transitive
 closure. Because of reflexivity, the future includes the present.
 
@@ -68,7 +68,7 @@
 fixed point (@{term lfp}) of @{term"\<lambda>T. mc f \<union> M\<inverse> `` T"} is the least set
 @{term T} containing @{term"mc f"} and all predecessors of @{term T}. If you
 find it hard to see that @{term"mc(EF f)"} contains exactly those states from
-which there is a path to a state where @{term f} is true, do not worry --- that
+which there is a path to a state where @{term f} is true, do not worry --- this
 will be proved in a moment.
 
 First we prove monotonicity of the function inside @{term lfp}
@@ -180,7 +180,7 @@
 text{*
 \begin{exercise}
 @{term AX} has a dual operator @{term EN}\footnote{We cannot use the customary @{text EX}
-as that is the ASCII equivalent of @{text"\<exists>"}}
+as that is the \textsc{ascii}-equivalent of @{text"\<exists>"}}
 (``there exists a next state such that'') with the intended semantics
 @{prop[display]"(s \<Turnstile> EN f) = (EX t. (s,t) : M & t \<Turnstile> f)"}
 Fortunately, @{term"EN f"} can already be expressed as a PDL formula. How?