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