--- a/doc-src/TutorialI/CTL/Base.thy Thu Jan 19 21:22:29 2006 +0100
+++ b/doc-src/TutorialI/CTL/Base.thy Thu Jan 19 21:22:30 2006 +0100
@@ -76,7 +76,7 @@
Finally we introduce a type of atomic propositions
*}
-typedecl atom
+typedecl "atom"
text{*\noindent
and a \emph{labelling function}