doc-src/TutorialI/CTL/document/CTLind.tex
changeset 10971 6852682eaf16
parent 10950 aa788fcb75a5
child 11196 bb4ede27fcb7
     1.1 --- a/doc-src/TutorialI/CTL/document/CTLind.tex	Wed Jan 24 11:59:15 2001 +0100
     1.2 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex	Wed Jan 24 12:29:10 2001 +0100
     1.3 @@ -128,7 +128,7 @@
     1.4  \isacommand{done}%
     1.5  \begin{isamarkuptext}%
     1.6  The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive means
     1.7 -that the assumption is left unchanged---otherwise the \isa{{\isasymforall}p} is turned
     1.8 +that the assumption is left unchanged --- otherwise the \isa{{\isasymforall}p} is turned
     1.9  into a \isa{{\isasymAnd}p}, which would complicate matters below. As it is,
    1.10  \isa{Avoid{\isacharunderscore}in{\isacharunderscore}lfp} is now
    1.11  \begin{isabelle}%