--- a/doc-src/TutorialI/CTL/document/CTLind.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTLind.tex Wed Jan 24 12:29:10 2001 +0100
@@ -128,7 +128,7 @@
\isacommand{done}%
\begin{isamarkuptext}%
The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive means
-that the assumption is left unchanged---otherwise the \isa{{\isasymforall}p} is turned
+that the assumption is left unchanged --- otherwise the \isa{{\isasymforall}p} is turned
into a \isa{{\isasymAnd}p}, which would complicate matters below. As it is,
\isa{Avoid{\isacharunderscore}in{\isacharunderscore}lfp} is now
\begin{isabelle}%