1.1 --- a/doc-src/TutorialI/CTL/document/PDL.tex	Fri Nov 24 16:49:27 2000 +0100
     1.2 +++ b/doc-src/TutorialI/CTL/document/PDL.tex	Sun Nov 26 10:48:38 2000 +0100
     1.3 @@ -21,7 +21,7 @@
     1.4  \noindent
     1.5  This is almost the same as in the boolean expression case study in
     1.6  \S\ref{sec:boolex}, except that what used to be called \isa{Var} is now
     1.7 -called \isa{formula{\isachardot}Atom}.
     1.8 +called \isa{Atom}.
     1.9  
    1.10  The meaning of these formulae is given by saying which formula is true in
    1.11  which state:%