--- a/doc-src/TutorialI/CTL/document/CTL.tex Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex Fri Jan 05 18:32:57 2001 +0100
@@ -281,7 +281,7 @@
\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma\ equalityI{\isacharbrackleft}OF\ AF{\isacharunderscore}lemma{\isadigit{1}}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharbrackright}{\isacharparenright}\isanewline
\isacommand{done}%
\begin{isamarkuptext}%
-The above language is not quite CTL. The latter also includes an
+The above language is not quite CTL\@. The latter also includes an
until-operator \isa{EU\ f\ g} with semantics ``there exist a path
where \isa{f} is true until \isa{g} becomes true''. With the help
of an auxiliary function%