--- a/doc-src/TutorialI/CTL/document/CTL.tex Tue Dec 11 17:07:45 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex Wed Dec 12 09:04:20 2001 +0100
@@ -469,7 +469,7 @@
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
+\isa{While{\isacharunderscore}Combinator} in the Library~\cite{HOL-Library} 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