# HG changeset patch
# User wenzelm
# Date 1137702150 -3600
# Node ID cb6e0064c88cea5d04a7da615acd293ba01cb0ec
# Parent  91d67d2f121c7d5ece9786e605eb15391d7ddb0d
quote "atom";

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}
diff -r 91d67d2f121c -r cb6e0064c88c doc-src/TutorialI/CTL/CTL.thy
--- a/doc-src/TutorialI/CTL/CTL.thy	Thu Jan 19 21:22:29 2006 +0100
+++ b/doc-src/TutorialI/CTL/CTL.thy	Thu Jan 19 21:22:30 2006 +0100
@@ -10,7 +10,7 @@
 @{text formula} by a new constructor
 *};
 (*<*)
-datatype formula = Atom atom
+datatype formula = Atom "atom"
                   | Neg formula
                   | And formula formula
                   | AX formula
diff -r 91d67d2f121c -r cb6e0064c88c doc-src/TutorialI/CTL/PDL.thy
--- a/doc-src/TutorialI/CTL/PDL.thy	Thu Jan 19 21:22:29 2006 +0100
+++ b/doc-src/TutorialI/CTL/PDL.thy	Thu Jan 19 21:22:30 2006 +0100
@@ -12,7 +12,7 @@
 shown to be equivalent.}
 *}
 
-datatype formula = Atom atom
+datatype formula = Atom "atom"
                   | Neg formula
                   | And formula formula
                   | AX formula
diff -r 91d67d2f121c -r cb6e0064c88c doc-src/TutorialI/CTL/document/PDL.tex
--- a/doc-src/TutorialI/CTL/document/PDL.tex	Thu Jan 19 21:22:29 2006 +0100
+++ b/doc-src/TutorialI/CTL/document/PDL.tex	Thu Jan 19 21:22:30 2006 +0100
@@ -31,7 +31,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{datatype}\isamarkupfalse%
-\ formula\ {\isacharequal}\ Atom\ atom\isanewline
+\ formula\ {\isacharequal}\ Atom\ {\isachardoublequoteopen}atom{\isachardoublequoteclose}\isanewline
 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Neg\ formula\isanewline
 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ And\ formula\ formula\isanewline
 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ AX\ formula\isanewline