--- a/doc-src/TutorialI/CTL/document/CTL.tex Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex Fri Nov 30 17:55:13 2001 +0100
@@ -465,15 +465,15 @@
\isamarkupfalse%
%
\begin{isamarkuptext}%
-Let us close this section with a few words about the executability of our model checkers.
-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.
-Fortunately, the
-Library\footnote{See theory \isa{While_Combinator}.}~\cite{isabelle-HOL-lib}
-provides a theorem stating that
-in the case of finite sets and a monotone function~\isa{F},
-the value of \mbox{\isa{lfp\ F}} can be computed by iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until
-a fixed point is reached. It is actually possible to generate executable functional programs
+Let us close this section with a few words about the executability of
+our model checkers. 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. Fortunately, theory
+\isa{While{\isacharunderscore}Combinator} in the Library~\cite{isabelle-HOL-lib} provides a
+theorem stating that in the case of finite sets and a monotone
+function~\isa{F}, the value of \mbox{\isa{lfp\ F}} can be computed by
+iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until a fixed point is
+reached. It is actually possible to generate executable functional programs
from HOL definitions, but that is beyond the scope of the tutorial.%
\index{CTL|)}%
\end{isamarkuptext}%