1.1 --- a/doc-src/TutorialI/CTL/document/CTLind.tex	Fri Jan 18 17:46:17 2002 +0100
     1.2 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex	Fri Jan 18 18:30:19 2002 +0100
     1.3 @@ -58,7 +58,7 @@
     1.4  \isamarkupfalse%
     1.5  \isacommand{apply}{\isacharparenleft}drule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}i{\isachardot}\ case\ i\ of\ {\isadigit{0}}\ {\isasymRightarrow}\ t\ {\isacharbar}\ Suc\ i\ {\isasymRightarrow}\ f\ i{\isachardoublequote}\ \isakeyword{in}\ bspec{\isacharparenright}\isanewline
     1.6  \isamarkupfalse%
     1.7 -\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}Paths{\isacharunderscore}def\ split{\isacharcolon}nat{\isachardot}split{\isacharparenright}\isanewline
     1.8 +\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ Paths{\isacharunderscore}def\ split{\isacharcolon}\ nat{\isachardot}split{\isacharparenright}\isanewline
     1.9  \isamarkupfalse%
    1.10  \isacommand{done}\isamarkupfalse%
    1.11  %
    1.12 @@ -133,7 +133,7 @@
    1.13  \ \isamarkupfalse%
    1.14  \isacommand{apply}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}\ add{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline
    1.15  \ \isamarkupfalse%
    1.16 -\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}\isamarkupfalse%
    1.17 +\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ Avoid{\isachardot}intros{\isacharparenright}\isamarkupfalse%
    1.18  %
    1.19  \begin{isamarkuptxt}%
    1.20  Having proved the main goal, we return to the proof obligation that the 
    1.21 @@ -149,13 +149,13 @@
    1.22  \isamarkuptrue%
    1.23  \isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}pp{\isacharparenright}\isanewline
    1.24  \isamarkupfalse%
    1.25 -\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain{\isacharparenright}\isanewline
    1.26 +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain{\isacharparenright}\isanewline
    1.27  \isamarkupfalse%
    1.28  \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
    1.29  \isamarkupfalse%
    1.30  \isacommand{apply}{\isacharparenleft}rule\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharparenright}\isanewline
    1.31  \isamarkupfalse%
    1.32 -\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharparenright}\isanewline
    1.33 +\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Paths{\isacharunderscore}def{\isacharparenright}\isanewline
    1.34  \isamarkupfalse%
    1.35  \isacommand{done}\isamarkupfalse%
    1.36  %
    1.37 @@ -177,7 +177,7 @@
    1.38  \isamarkuptrue%
    1.39  \isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\ \ {\isachardoublequote}{\isacharbraceleft}s{\isachardot}\ {\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}\ {\isasymsubseteq}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline
    1.40  \isamarkupfalse%
    1.41 -\isacommand{by}{\isacharparenleft}auto\ elim{\isacharcolon}Avoid{\isacharunderscore}in{\isacharunderscore}lfp\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}\isanewline
    1.42 +\isacommand{by}{\isacharparenleft}auto\ elim{\isacharcolon}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp\ intro{\isacharcolon}\ Avoid{\isachardot}intros{\isacharparenright}\isanewline
    1.43  \isanewline
    1.44  \isamarkupfalse%
    1.45  \isamarkupfalse%