--- a/doc-src/TutorialI/CTL/CTL.thy Wed Dec 13 09:32:55 2000 +0100
+++ b/doc-src/TutorialI/CTL/CTL.thy Wed Dec 13 09:39:53 2000 +0100
@@ -182,7 +182,7 @@
text{*\noindent
Element @{term"n+1"} on this path is some arbitrary successor
@{term t} of element @{term n} such that @{term"P t"} holds. Remember that @{text"SOME t. R t"}
-is some arbitrary but fixed @{term t} such that @{prop"R t"} holds (see \S\ref{sec-SOME}). Of
+is some arbitrary but fixed @{term t} such that @{prop"R t"} holds (see \S\ref{sec:SOME}). Of
course, such a @{term t} may in general not exist, but that is of no
concern to us since we will only use @{term path} in such cases where a
suitable @{term t} does exist.