diff -r e928bdf62014 -r e61e7e1eacaf doc-src/TutorialI/CTL/CTL.thy
--- a/doc-src/TutorialI/CTL/CTL.thy	Fri Oct 13 11:15:56 2000 +0200
+++ b/doc-src/TutorialI/CTL/CTL.thy	Fri Oct 13 18:02:08 2000 +0200
@@ -364,9 +364,13 @@
 done;
 
 text{*
-The main theorem is proved as for PDL, except that we also derive the necessary equality
-@{text"lfp(af A) = ..."} by combining @{thm[source]AF_lemma1} and @{thm[source]AF_lemma2}
-on the spot:
+If you found the above proofs somewhat complicated we recommend you read
+\S\ref{sec:CTL-revisited} where we shown how inductive definitions lead to
+simpler arguments.
+
+The main theorem is proved as for PDL, except that we also derive the
+necessary equality @{text"lfp(af A) = ..."} by combining
+@{thm[source]AF_lemma1} and @{thm[source]AF_lemma2} on the spot:
 *}
 
 theorem "mc f = {s. s \<Turnstile> f}";