1.1 --- a/doc-src/TutorialI/CTL/document/CTLind.tex	Tue May 01 17:16:32 2001 +0200
     1.2 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex	Tue May 01 22:26:55 2001 +0200
     1.3 @@ -59,9 +59,9 @@
     1.4  and that the instantiated induction hypothesis implies the conclusion.
     1.5  
     1.6  Now we come to the key lemma. Assuming that no infinite \isa{A}-avoiding
     1.7 -path starts from \isa{s}, we want to show \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. This
     1.8 -can be generalized by proving that every point \isa{t} ``between''
     1.9 -\isa{s} and \isa{A}, i.e.\ all of \isa{Avoid\ s\ A},
    1.10 +path starts from \isa{s}, we want to show \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. For the
    1.11 +inductive proof this must be generalized to the statement that every point \isa{t}
    1.12 +``between'' \isa{s} and \isa{A}, i.e.\ all of \isa{Avoid\ s\ A},
    1.13  is contained in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}:%
    1.14  \end{isamarkuptext}%
    1.15  \isacommand{lemma}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline
    1.16 @@ -79,7 +79,7 @@
    1.17  \begin{isabelle}%
    1.18  \ \ \ \ \ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}%
    1.19  \end{isabelle}
    1.20 -As we shall see in a moment, the absence of infinite \isa{A}-avoiding paths
    1.21 +As we shall see presently, the absence of infinite \isa{A}-avoiding paths
    1.22  starting from \isa{s} implies well-foundedness of this relation. For the
    1.23  moment we assume this and proceed with the induction:%
    1.24  \end{isamarkuptxt}%