--- a/doc-src/TutorialI/CTL/Base.thy	Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/CTL/Base.thy	Thu May 29 22:45:33 2008 +0200
@@ -72,7 +72,7 @@
 consts M :: "(state \<times> state)set";
 
 text{*\noindent
-Again, we could have made @{term 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
 *}