--- a/doc-src/Codegen/Thy/document/Evaluation.tex Mon Sep 27 16:19:37 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex Mon Sep 27 16:27:31 2010 +0200
@@ -269,7 +269,20 @@
%
\isatagquote
\isacommand{datatype}\isamarkupfalse%
-\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\ \ \isacommand{ML}\isamarkupfalse%
+\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\ %
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isadelimquotett
+\ %
+\endisadelimquotett
+%
+\isatagquotett
+\isacommand{ML}\isamarkupfalse%
\ {\isacharverbatimopen}\isanewline
\ \ fun\ eval{\isacharunderscore}form\ %
\isaantiq
@@ -294,12 +307,12 @@
\ {\isacharparenleft}p{\isacharcomma}\ q{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ \ \ \ \ eval{\isacharunderscore}form\ p\ orelse\ eval{\isacharunderscore}form\ q{\isacharsemicolon}\isanewline
{\isacharverbatimclose}%
-\endisatagquote
-{\isafoldquote}%
+\endisatagquotett
+{\isafoldquotett}%
%
-\isadelimquote
+\isadelimquotett
%
-\endisadelimquote
+\endisadelimquotett
%
\begin{isamarkuptext}%
\noindent \isa{code} takes as argument the name of a constant;