diff -r 91d67d2f121c -r cb6e0064c88c doc-src/TutorialI/CTL/Base.thy
--- 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}