# HG changeset patch
# User wenzelm
# Date 1137702149 -3600
# Node ID 91d67d2f121c7d5ece9786e605eb15391d7ddb0d
# Parent  0888eca0f1be41fd44f7d5accae3cf48d590acc4
updated;

diff -r 0888eca0f1be -r 91d67d2f121c doc-src/LaTeXsugar/Sugar/document/Sugar.tex
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Thu Jan 19 21:22:27 2006 +0100
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Thu Jan 19 21:22:29 2006 +0100
@@ -492,7 +492,7 @@
     \verb!setup {!\verb!*!\\
     \verb!let!\\
     \verb!  fun my_concl ctxt = Logic.strip_imp_concl!\\
-    \verb!  in [TermStyle.add_style "my_concl" my_concl]!\\
+    \verb!  in TermStyle.add_style "my_concl" my_concl!\\
     \verb!end;!\\
     \verb!*!\verb!}!\\
   \end{quote}
diff -r 0888eca0f1be -r 91d67d2f121c doc-src/TutorialI/CTL/document/Base.tex
--- a/doc-src/TutorialI/CTL/document/Base.tex	Thu Jan 19 21:22:27 2006 +0100
+++ b/doc-src/TutorialI/CTL/document/Base.tex	Thu Jan 19 21:22:29 2006 +0100
@@ -97,7 +97,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{typedecl}\isamarkupfalse%
-\ atom%
+\ {\isachardoublequoteopen}atom{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \noindent
 and a \emph{labelling function}%