diff -r dfff821d2949 -r 59d6633835fa doc-src/TutorialI/CTL/document/CTL.tex
--- a/doc-src/TutorialI/CTL/document/CTL.tex	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/CTL/document/CTL.tex	Mon Oct 09 10:18:21 2000 +0200
@@ -188,7 +188,7 @@
 holds. However, we first have to show that such a \isa{t} actually exists! This reasoning
 is embodied in the theorem \isa{someI\isadigit{2}{\isacharunderscore}ex}:
 \begin{isabelle}%
-\ \ \ \ \ {\isasymlbrakk}{\isasymexists}a{\isachardot}\ {\isacharquery}P\ a{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q\ {\isacharparenleft}Eps\ {\isacharquery}P{\isacharparenright}%
+\ \ \ \ \ {\isasymlbrakk}{\isasymexists}a{\isachardot}\ {\isacharquery}P\ a{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q\ {\isacharparenleft}SOME\ x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}%
 \end{isabelle}
 When we apply this theorem as an introduction rule, \isa{{\isacharquery}P\ x} becomes
 \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ x} and \isa{{\isacharquery}Q\ x} becomes \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M} and we have to prove
@@ -220,14 +220,15 @@
 \begin{isamarkuptext}%
 Function \isa{path} has fulfilled its purpose now and can be forgotten
 about. It was merely defined to provide the witness in the proof of the
-\isa{infinity{\isacharunderscore}lemma}. Afficionados of minimal proofs might like to know
+\isa{infinity{\isacharunderscore}lemma}. Aficionados of minimal proofs might like to know
 that we could have given the witness without having to define a new function:
 the term
 \begin{isabelle}%
 \ \ \ \ \ nat{\isacharunderscore}rec\ s\ {\isacharparenleft}{\isasymlambda}n\ t{\isachardot}\ SOME\ u{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ u{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ u{\isacharparenright}%
 \end{isabelle}
+is extensionally equal to \isa{path\ s\ P},
 where \isa{nat{\isacharunderscore}rec} is the predefined primitive recursor on \isa{nat}, whose defining
-equations we omit, is extensionally equal to \isa{path\ s\ P}.%
+equations we omit.%
 \end{isamarkuptext}%
 %
 \begin{isamarkuptext}%
@@ -271,6 +272,22 @@
 \isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma\ equalityI{\isacharbrackleft}OF\ AF{\isacharunderscore}lemma\isadigit{1}\ AF{\isacharunderscore}lemma\isadigit{2}{\isacharbrackright}{\isacharparenright}\isanewline
 \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}''.
+It is not definable in terms of the other operators!
+\begin{exercise}
+Extend the datatype of formulae by the until operator with semantics
+\begin{isabelle}%
+\ \ \ \ \ s\ {\isasymTurnstile}\ f\ U\ g\ {\isacharequal}\ {\isacharparenleft}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\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}%
+\end{isabelle}
+Prove that the equivalence between semantics and model checking still holds.
+\end{exercise}
+
 Let us close this section with a few words about the executability of \isa{mc}.
 It is clear that if all sets are finite, they can be represented as lists and the usual
 set operations are easily implemented. Only \isa{lfp} requires a little thought.