diff -r dfff821d2949 -r 59d6633835fa doc-src/TutorialI/CTL/CTL.thy
--- a/doc-src/TutorialI/CTL/CTL.thy	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/CTL/CTL.thy	Mon Oct 09 10:18:21 2000 +0200
@@ -291,12 +291,13 @@
 text{*
 Function @{term path} has fulfilled its purpose now and can be forgotten
 about. It was merely defined to provide the witness in the proof of the
-@{thm[source]infinity_lemma}. Afficionados of minimal proofs might like to know
+@{thm[source]infinity_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
 @{term[display]"nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> P u)"}
+is extensionally equal to @{term"path s P"},
 where @{term nat_rec} is the predefined primitive recursor on @{typ nat}, whose defining
-equations we omit, is extensionally equal to @{term"path s P"}.
+equations we omit.
 *};
 (*<*)
 lemma infinity_lemma:
@@ -372,6 +373,18 @@
 done
 
 text{*
+The above language is not quite CTL. The latter also includes an
+until-operator, usually written as an infix @{text U}. The formula
+@{term"f U g"} means ``@{term f} until @{term g}''.
+It is not definable in terms of the other operators!
+\begin{exercise}
+Extend the datatype of formulae by the until operator with semantics
+@{text[display]"s \<Turnstile> f U g = (............)"}
+and model checking algorithm
+@{text[display]"mc(f U g) = (............)"}
+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 @{term 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 @{term lfp} requires a little thought.