doc-src/TutorialI/CTL/CTL.thy

--- a/doc-src/TutorialI/CTL/CTL.thy	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/CTL/CTL.thy	Fri Jan 05 18:32:57 2001 +0100
@@ -346,7 +346,7 @@
 
 text{*
 
-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 @{term"EU f g"} with semantics ``there exist a path
 where @{term f} is true until @{term g} becomes true''. With the help
 of an auxiliary function