diff -r a5f53d9d2b60 -r f8537d69f514 doc-src/TutorialI/CTL/document/Base.tex
--- a/doc-src/TutorialI/CTL/document/Base.tex	Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/CTL/document/Base.tex	Thu May 29 22:45:33 2008 +0200
@@ -92,7 +92,7 @@
 \ M\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}state\ {\isasymtimes}\ state{\isacharparenright}set{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \noindent
-Again, we could have made \isa{M} a parameter of everything.
+This is Isabelle's way of declaring a constant without defining it.
 Finally we introduce a type of atomic propositions%
 \end{isamarkuptext}%
 \isamarkuptrue%