summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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.