doc-src/TutorialI/CTL/CTL.thy
changeset 10654 458068404143
parent 10363 6e8002c1790e
child 10795 9e888d60d3e5
     1.1 --- a/doc-src/TutorialI/CTL/CTL.thy	Wed Dec 13 09:32:55 2000 +0100
     1.2 +++ b/doc-src/TutorialI/CTL/CTL.thy	Wed Dec 13 09:39:53 2000 +0100
     1.3 @@ -182,7 +182,7 @@
     1.4  text{*\noindent
     1.5  Element @{term"n+1"} on this path is some arbitrary successor
     1.6  @{term t} of element @{term n} such that @{term"P t"} holds.  Remember that @{text"SOME t. R t"}
     1.7 -is some arbitrary but fixed @{term t} such that @{prop"R t"} holds (see \S\ref{sec-SOME}). Of
     1.8 +is some arbitrary but fixed @{term t} such that @{prop"R t"} holds (see \S\ref{sec:SOME}). Of
     1.9  course, such a @{term t} may in general not exist, but that is of no
    1.10  concern to us since we will only use @{term path} in such cases where a
    1.11  suitable @{term t} does exist.