diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/CTL/CTLind.thy
--- a/doc-src/TutorialI/CTL/CTLind.thy	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/CTL/CTLind.thy	Fri Jan 05 18:32:57 2001 +0100
@@ -7,7 +7,7 @@
 some of the induction principles and heuristics discussed above and we want to
 show how inductive definitions can simplify proofs.
 In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a
-model checker for CTL. In particular the proof of the
+model checker for CTL\@. In particular the proof of the
 @{thm[source]infinity_lemma} on the way to @{thm[source]AF_lemma2} is not as
 simple as one might intuitively expect, due to the @{text SOME} operator
 involved. Below we give a simpler proof of @{thm[source]AF_lemma2}