
diff -r 2995639c6a09 -r 90695f46440b doc-src/TutorialI/CTL/CTL.thy
--- a/doc-src/TutorialI/CTL/CTL.thy	Fri Jan 12 16:28:14 2001 +0100
+++ b/doc-src/TutorialI/CTL/CTL.thy	Fri Jan 12 16:32:01 2001 +0100
@@ -456,10 +456,10 @@
 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 @{term lfp} requires a little thought.
-\REMARK{you had `in the library' but I assume you meant it was a 
-built in lemma.  Do we give its name?}
-Fortunately, Isabelle/HOL provides a theorem stating that 
-in the case of finite sets and a monotone @{term F},
+Fortunately, the HOL Library%
+\footnote{See theory \isa{While_Combinator_Example}.}
+provides a theorem stating that 
+in the case of finite sets and a monotone function~@{term F},
 the value of @{term"lfp F"} can be computed by iterated application of @{term F} to~@{term"{}"} 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.




