--- 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%