doc-src/Codegen/Thy/document/Adaptation.tex

   additionally, eager evaluation may cause programs to loop or break
   which would perfectly terminate when the existing SML \verb|bool| would be used.  To map the HOL \isa{bool} on SML \verb|bool|, we may use \qn{custom serialisations}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\isatagquotett
+\isadelimtt
+%
+\endisadelimtt
+%
+\isatagtt
 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
 \ bool\isanewline
 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}bool{\isachardoublequoteclose}{\isacharparenright}\isanewline
 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
 \ True\ \isakeyword{and}\ False\ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}true{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}false{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isacharunderscore}\ andalso\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
-%
-\isadelimquotett
-%
-\endisadelimquotett
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+%
+\endisadelimtt
 %
 \begin{isamarkuptext}%
 \noindent The \indexdef{}{command}{code\_type}\hypertarget{command.code-type}{\hyperlink{command.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}} command takes a type constructor
   as arguments together with a list of custom serialisations.  Each
   custom serialisation starts with a target language identifier

   provides some common idioms, notably associative infixes with
   precedences which may be used here:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\isatagquotett
+\isadelimtt
+%
+\endisadelimtt
+%
+\isatagtt
 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
 \ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
 \ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
-%
-\isadelimquotett
-%
-\endisadelimquotett
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+%
+\endisadelimtt
 %
 \isadelimtypewriter
 %
 \endisadelimtypewriter
 %

 %
 \isadeliminvisible
 %
 \endisadeliminvisible
 %
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\isatagquotett
+\isadelimtt
+%
+\endisadelimtt
+%
+\isatagtt
 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
 \ prod\isanewline
 \ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline
 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
 \ Pair\isanewline
 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
-%
-\isadelimquotett
-%
-\endisadelimquotett
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+%
+\endisadelimtt
 %
 \begin{isamarkuptext}%
 \noindent The initial bang ``\verb|!|'' tells the serialiser
   never to put parentheses around the whole expression (they are
   already present), while the parentheses around argument place

   giving custom serialisations for the class \isa{equal} (by command
   \indexdef{}{command}{code\_class}\hypertarget{command.code-class}{\hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}}) and its operation \isa{HOL{\isachardot}equal}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\isatagquotett
+\isadelimtt
+%
+\endisadelimtt
+%
+\isatagtt
 \isacommand{code{\isacharunderscore}class}\isamarkupfalse%
 \ equal\isanewline
 \ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}{\isacharparenright}\isanewline
 \isanewline
 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
 \ {\isachardoublequoteopen}HOL{\isachardot}equal{\isachardoublequoteclose}\isanewline
 \ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
-%
-\isadelimquotett
-%
-\endisadelimquotett
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+%
+\endisadelimtt
 %
 \begin{isamarkuptext}%
 \noindent A problem now occurs whenever a type which is an instance
   of \isa{equal} in \isa{HOL} is mapped on a \isa{Haskell}-built-in type which is also an instance of \isa{Haskell}
   \isa{Eq}:%

 %
 \isadelimquote
 %
 \endisadelimquote
 %
-\isadelimquotett
+\isadelimtt
 \ %
-\endisadelimquotett
-%
-\isatagquotett
+\endisadelimtt
+%
+\isatagtt
 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
 \ bar\isanewline
 \ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
-%
-\isadelimquotett
-%
-\endisadelimquotett
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+%
+\endisadelimtt
 %
 \begin{isamarkuptext}%
 \noindent The code generator would produce an additional instance,
   which of course is rejected by the \isa{Haskell} compiler.  To
   suppress this additional instance, use \indexdef{}{command}{code\_instance}\hypertarget{command.code-instance}{\hyperlink{command.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\isatagquotett
+\isadelimtt
+%
+\endisadelimtt
+%
+\isatagtt
 \isacommand{code{\isacharunderscore}instance}\isamarkupfalse%
 \ bar\ {\isacharcolon}{\isacharcolon}\ equal\isanewline
 \ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
-%
-\isadelimquotett
-%
-\endisadelimquotett
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+%
+\endisadelimtt
 %
 \isamarkupsubsection{Enhancing the target language context \label{sec:include}%
 }
 \isamarkuptrue%
 %

 In rare cases it is necessary to \emph{enrich} the context of a
   target language; this is accomplished using the \indexdef{}{command}{code\_include}\hypertarget{command.code-include}{\hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}} command:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\isatagquotett
+\isadelimtt
+%
+\endisadelimtt
+%
+\isatagtt
 \isacommand{code{\isacharunderscore}include}\isamarkupfalse%
 \ Haskell\ {\isachardoublequoteopen}Errno{\isachardoublequoteclose}\isanewline
 {\isacharverbatimopen}errno\ i\ {\isacharequal}\ error\ {\isacharparenleft}{\isachardoublequote}Error\ number{\isacharcolon}\ {\isachardoublequote}\ {\isacharplus}{\isacharplus}\ show\ i{\isacharparenright}{\isacharverbatimclose}\isanewline
 \isanewline
 \isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
 \ Haskell\ Errno%
-\endisatagquotett
-{\isafoldquotett}%
-%
-\isadelimquotett
-%
-\endisadelimquotett
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+%
+\endisadelimtt
 %
 \begin{isamarkuptext}%
 \noindent Such named \isa{include}s are then prepended to every
   generated code.  Inspect such code in order to find out how
   \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} behaves with respect to a particular