--- a/doc-src/TutorialI/CTL/document/CTL.tex Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex Thu Nov 29 21:12:37 2001 +0100
@@ -468,8 +468,8 @@
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 HOL Library%
-\footnote{See theory \isa{While_Combinator}.}
+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