1.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex	Fri Nov 30 12:18:14 2001 +0100
     1.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex	Fri Nov 30 17:55:13 2001 +0100
     1.3 @@ -465,15 +465,15 @@
     1.4  \isamarkupfalse%
     1.5  %
     1.6  \begin{isamarkuptext}%
     1.7 -Let us close this section with a few words about the executability of our model checkers.
     1.8 -It is clear that if all sets are finite, they can be represented as lists and the usual
     1.9 -set operations are easily implemented. Only \isa{lfp} requires a little thought.
    1.10 -Fortunately, the
    1.11 -Library\footnote{See theory \isa{While_Combinator}.}~\cite{isabelle-HOL-lib}
    1.12 -provides a theorem stating that 
    1.13 -in the case of finite sets and a monotone function~\isa{F},
    1.14 -the value of \mbox{\isa{lfp\ F}} can be computed by iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until
    1.15 -a fixed point is reached. It is actually possible to generate executable functional programs
    1.16 +Let us close this section with a few words about the executability of
    1.17 +our model checkers.  It is clear that if all sets are finite, they can be
    1.18 +represented as lists and the usual set operations are easily
    1.19 +implemented. Only \isa{lfp} requires a little thought.  Fortunately, theory
    1.20 +\isa{While{\isacharunderscore}Combinator} in the Library~\cite{isabelle-HOL-lib} provides a
    1.21 +theorem stating that in the case of finite sets and a monotone
    1.22 +function~\isa{F}, the value of \mbox{\isa{lfp\ F}} can be computed by
    1.23 +iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until a fixed point is
    1.24 +reached. It is actually possible to generate executable functional programs
    1.25  from HOL definitions, but that is beyond the scope of the tutorial.%
    1.26  \index{CTL|)}%
    1.27  \end{isamarkuptext}%