diff -r 383b0a1837a9 -r aecb5bf6f76f doc-src/TutorialI/CTL/document/CTL.tex
--- a/doc-src/TutorialI/CTL/document/CTL.tex	Mon Oct 09 17:40:47 2000 +0200
+++ b/doc-src/TutorialI/CTL/document/CTL.tex	Mon Oct 09 19:20:55 2000 +0200
@@ -66,8 +66,6 @@
 \isacommand{apply}{\isacharparenleft}clarsimp\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
-FIXME OF/of with undescore?
-
 leads to the following somewhat involved proof state
 \begin{isabelle}
 \ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ \isadigit{0}\ {\isasymin}\ A\ {\isasymor}\isanewline
@@ -273,19 +271,23 @@
 \isacommand{done}%
 \begin{isamarkuptext}%
 The above language is not quite CTL. The latter also includes an
-until-operator, usually written as an infix \isa{U}. The formula
-\isa{f\ U\ g} means ``\isa{f} until \isa{g}''.
+until-operator, which is the subject of the following exercise.
 It is not definable in terms of the other operators!
 \begin{exercise}
-Extend the datatype of formulae by the until operator with semantics
+Extend the datatype of formulae by the binary until operator \isa{EU\ f\ g} with semantics
+``there exist a path where \isa{f} is true until \isa{g} becomes true''
 \begin{isabelle}%
-\ \ \ \ \ s\ {\isasymTurnstile}\ f\ U\ g\ {\isacharequal}\ {\isacharparenleft}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isacharparenright}%
+\ \ \ \ \ s\ {\isasymTurnstile}\ EU\ f\ g\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}j{\isachardot}\ p\ j\ {\isasymTurnstile}\ g\ {\isasymand}\ {\isacharparenleft}{\isasymexists}i\ {\isacharless}\ j{\isachardot}\ p\ i\ {\isasymTurnstile}\ f{\isacharparenright}{\isacharparenright}%
 \end{isabelle}
 and model checking algorithm
 \begin{isabelle}%
-\ \ \ \ \ mc{\isacharparenleft}f\ U\ g{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isacharparenright}%
+\ \ \ \ \ mc{\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ g\ {\isasymunion}\ mc\ f\ {\isasyminter}\ {\isacharparenleft}M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}{\isacharparenright}%
 \end{isabelle}
-Prove that the equivalence between semantics and model checking still holds.
+Prove the equivalence between semantics and model checking, i.e.\
+\isa{mc\ {\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ EU\ f\ g{\isacharbraceright}}.
+
+For readability you may want to equip \isa{EU} with the following customary syntax:
+\isa{E{\isacharbrackleft}f\ U\ g{\isacharbrackright}}.
 \end{exercise}
 
 Let us close this section with a few words about the executability of \isa{mc}.