%

\begin{isabellebody}%

\def\isabellecontext{Adaption}%

%

\isadelimtheory

%

\endisadelimtheory

%

\isatagtheory

\isacommand{theory}\isamarkupfalse%

\ Adaption\isanewline

\isakeyword{imports}\ Setup\isanewline

\isakeyword{begin}%

\endisatagtheory

{\isafoldtheory}%

%

\isadelimtheory

\isanewline

%

\endisadelimtheory

%

\isadeliminvisible

\isanewline

%

\endisadeliminvisible

%

\isataginvisible

\isacommand{setup}\isamarkupfalse%

\ {\isacharverbatimopen}\ Code{\isacharunderscore}Target{\isachardot}extend{\isacharunderscore}target\ {\isacharparenleft}{\isachardoublequote}{\isasymSML}{\isachardoublequote}{\isacharcomma}\ {\isacharparenleft}{\isachardoublequote}SML{\isachardoublequote}{\isacharcomma}\ K\ I{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}%

\endisataginvisible

{\isafoldinvisible}%

%

\isadeliminvisible

%

\endisadeliminvisible

%

\isamarkupsection{Adaption to target languages \label{sec:adaption}%

}

\isamarkuptrue%

%

\isamarkupsubsection{Adapting code generation%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

The aspects of code generation introduced so far have two aspects

  in common:

  \begin{itemize}

    \item They act uniformly, without reference to a specific

       target language.

    \item They are \emph{safe} in the sense that as long as you trust

       the code generator meta theory and implementation, you cannot

       produce programs that yield results which are not derivable

       in the logic.

  \end{itemize}

  \noindent In this section we will introduce means to \emph{adapt} the serialiser

  to a specific target language, i.e.~to print program fragments

  in a way which accommodates \qt{already existing} ingredients of

  a target language environment, for three reasons:

  \begin{itemize}

    \item improving readability and aesthetics of generated code

    \item gaining efficiency

    \item interface with language parts which have no direct counterpart

      in \isa{HOL} (say, imperative data structures)

  \end{itemize}

  \noindent Generally, you should avoid using those features yourself

  \emph{at any cost}:

  \begin{itemize}

    \item The safe configuration methods act uniformly on every target language,

      whereas for adaption you have to treat each target language separate.

    \item Application is extremely tedious since there is no abstraction

      which would allow for a static check, making it easy to produce garbage.

    \item More or less subtle errors can be introduced unconsciously.

  \end{itemize}

  \noindent However, even if you ought refrain from setting up adaption

  yourself, already the \isa{HOL} comes with some reasonable default

  adaptions (say, using target language list syntax).  There also some

  common adaption cases which you can setup by importing particular

  library theories.  In order to understand these, we provide some clues here;

  these however are not supposed to replace a careful study of the sources.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{The adaption principle%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

Figure \ref{fig:adaption} illustrates what \qt{adaption} is conceptually

  supposed to be:

  \begin{figure}[here]

    \includegraphics{Thy/pictures/adaption}

    \caption{The adaption principle}

    \label{fig:adaption}

  \end{figure}

  \noindent In the tame view, code generation acts as broker between

  \isa{logic}, \isa{intermediate\ language} and

  \isa{target\ language} by means of \isa{translation} and

  \isa{serialisation};  for the latter, the serialiser has to observe

  the structure of the \isa{language} itself plus some \isa{reserved}

  keywords which have to be avoided for generated code.

  However, if you consider \isa{adaption} mechanisms, the code generated

  by the serializer is just the tip of the iceberg:

  \begin{itemize}

    \item \isa{serialisation} can be \emph{parametrised} such that

      logical entities are mapped to target-specific ones

      (e.g. target-specific list syntax,

        see also \secref{sec:adaption_mechanisms})

    \item Such parametrisations can involve references to a

      target-specific standard \isa{library} (e.g. using

      the \isa{Haskell} \verb|Maybe| type instead

      of the \isa{HOL} \isa{option} type);

      if such are used, the corresponding identifiers

      (in our example, \verb|Maybe|, \verb|Nothing|

      and \verb|Just|) also have to be considered \isa{reserved}.

    \item Even more, the user can enrich the library of the

      target-language by providing code snippets

      (\qt{\isa{includes}}) which are prepended to

      any generated code (see \secref{sec:include});  this typically

      also involves further \isa{reserved} identifiers.

  \end{itemize}

  \noindent As figure \ref{fig:adaption} illustrates, all these adaption mechanisms

  have to act consistently;  it is at the discretion of the user

  to take care for this.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{Common adaption patterns%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

The \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \hyperlink{theory.Main}{\mbox{\isa{Main}}} theory already provides a code

  generator setup

  which should be suitable for most applications.  Common extensions

  and modifications are available by certain theories of the \isa{HOL}

  library; beside being useful in applications, they may serve

  as a tutorial for customising the code generator setup (see below

  \secref{sec:adaption_mechanisms}).

  \begin{description}

    \item[\hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}] represents \isa{HOL} integers by big

       integer literals in target languages.

    \item[\hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}] represents \isa{HOL} characters by 

       character literals in target languages.

    \item[\hyperlink{theory.Code-Char-chr}{\mbox{\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}}}] like \isa{Code{\isacharunderscore}Char},

       but also offers treatment of character codes; includes

       \hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}.

    \item[\hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}Nat}}}] \label{eff_nat} implements natural numbers by integers,

       which in general will result in higher efficiency; pattern

       matching with \isa{{\isadigit{0}}} / \isa{Suc}

       is eliminated;  includes \hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}

       and \hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}.

    \item[\hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}] provides an additional datatype

       \isa{index} which is mapped to target-language built-in integers.

       Useful for code setups which involve e.g. indexing of

       target-language arrays.

    \item[\hyperlink{theory.Code-Message}{\mbox{\isa{Code{\isacharunderscore}Message}}}] provides an additional datatype

       \isa{message{\isacharunderscore}string} which is isomorphic to strings;

       \isa{message{\isacharunderscore}string}s are mapped to target-language strings.

       Useful for code setups which involve e.g. printing (error) messages.

  \end{description}

  \begin{warn}

    When importing any of these theories, they should form the last

    items in an import list.  Since these theories adapt the

    code generator setup in a non-conservative fashion,

    strange effects may occur otherwise.

  \end{warn}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{Parametrising serialisation \label{sec:adaption_mechanisms}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

Consider the following function and its corresponding

  SML code:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

\isacommand{primrec}\isamarkupfalse%

\ in{\isacharunderscore}interval\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline

\ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\isadeliminvisible

%

\endisadeliminvisible

%

\isataginvisible

%

\endisataginvisible

{\isafoldinvisible}%

%

\isadeliminvisible

%

\endisadeliminvisible

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

%

\begin{isamarkuptext}%

\isatypewriter%

\noindent%

\hspace*{0pt}structure Example = \\

\hspace*{0pt}struct\\

\hspace*{0pt}\\

\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\

\hspace*{0pt}\\

\hspace*{0pt}datatype boola = True | False;\\

\hspace*{0pt}\\

\hspace*{0pt}fun anda x True = x\\

\hspace*{0pt} ~| anda x False = False\\

\hspace*{0pt} ~| anda True x = x\\

\hspace*{0pt} ~| anda False x = False;\\

\hspace*{0pt}\\

\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\

\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = False\\

\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\

\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = True;\\

\hspace*{0pt}\\

\hspace*{0pt}fun in{\char95}interval (k,~l) n = anda (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\

\hspace*{0pt}\\

\hspace*{0pt}end;~(*struct Example*)%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\begin{isamarkuptext}%

\noindent Though this is correct code, it is a little bit unsatisfactory:

  boolean values and operators are materialised as distinguished

  entities with have nothing to do with the SML-built-in notion

  of \qt{bool}.  This results in less readable code;

  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

\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

%

\begin{isamarkuptext}%

\noindent The \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 followed by an expression, which during

  code serialisation is inserted whenever the type constructor

  would occur.  For constants, \hyperlink{command.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} implements

  the corresponding mechanism.  Each ``\verb|_|'' in

  a serialisation expression is treated as a placeholder

  for the type constructor's (the constant's) arguments.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

%

\begin{isamarkuptext}%

\isatypewriter%

\noindent%

\hspace*{0pt}structure Example = \\

\hspace*{0pt}struct\\

\hspace*{0pt}\\

\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\

\hspace*{0pt}\\

\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\

\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\

\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\

\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\

\hspace*{0pt}\\

\hspace*{0pt}fun in{\char95}interval (k,~l) n = (less{\char95}eq{\char95}nat k n) andalso (less{\char95}eq{\char95}nat n l);\\

\hspace*{0pt}\\

\hspace*{0pt}end;~(*struct Example*)%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\begin{isamarkuptext}%

\noindent This still is not perfect: the parentheses

  around the \qt{andalso} expression are superfluous.

  Though the serialiser

  by no means attempts to imitate the rich Isabelle syntax

  framework, it provides some common idioms, notably

  associative infixes with precedences which may be used here:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquotett

%

\endisadelimquotett

%

\isatagquotett

\isacommand{code{\isacharunderscore}const}\isamarkupfalse%

\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline

\ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}%

\endisatagquotett

{\isafoldquotett}%

%

\isadelimquotett

%

\endisadelimquotett

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

%

\begin{isamarkuptext}%

\isatypewriter%

\noindent%

\hspace*{0pt}structure Example = \\

\hspace*{0pt}struct\\

\hspace*{0pt}\\

\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\

\hspace*{0pt}\\

\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\

\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\

\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\

\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\

\hspace*{0pt}\\

\hspace*{0pt}fun in{\char95}interval (k,~l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\

\hspace*{0pt}\\

\hspace*{0pt}end;~(*struct Example*)%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\begin{isamarkuptext}%

\noindent The attentive reader may ask how we assert that no generated

  code will accidentally overwrite.  For this reason the serialiser has

  an internal table of identifiers which have to be avoided to be used

  for new declarations.  Initially, this table typically contains the

  keywords of the target language.  It can be extended manually, thus avoiding

  accidental overwrites, using the \hyperlink{command.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} command:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

\isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%

\ {\isachardoublequoteopen}{\isasymSML}{\isachardoublequoteclose}\ bool\ true\ false\ andalso%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\begin{isamarkuptext}%

\noindent Next, we try to map HOL pairs to SML pairs, using the

  infix ``\verb|*|'' type constructor and parentheses:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadeliminvisible

%

\endisadeliminvisible

%

\isataginvisible

%

\endisataginvisible

{\isafoldinvisible}%

%

\isadeliminvisible

%

\endisadeliminvisible

%

\isadelimquotett

%

\endisadelimquotett

%

\isatagquotett

\isacommand{code{\isacharunderscore}type}\isamarkupfalse%

\ {\isacharasterisk}\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

%

\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 holders

  tell not to put parentheses around the arguments.

  The slash ``\verb|/|'' (followed by arbitrary white space)

  inserts a space which may be used as a break if necessary

  during pretty printing.

  These examples give a glimpse what mechanisms

  custom serialisations provide; however their usage

  requires careful thinking in order not to introduce

  inconsistencies -- or, in other words:

  custom serialisations are completely axiomatic.

  A further noteworthy details is that any special

  character in a custom serialisation may be quoted

  using ``\verb|'|''; thus, in

  ``\verb|fn '_ => _|'' the first

  ``\verb|_|'' is a proper underscore while the

  second ``\verb|_|'' is a placeholder.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{\isa{Haskell} serialisation%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

For convenience, the default

  \isa{HOL} setup for \isa{Haskell} maps the \isa{eq} class to

  its counterpart in \isa{Haskell}, giving custom serialisations

  for the class \isa{eq} (by command \hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}) and its operation

  \isa{eq{\isacharunderscore}class{\isachardot}eq}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquotett

%

\endisadelimquotett

%

\isatagquotett

\isacommand{code{\isacharunderscore}class}\isamarkupfalse%

\ eq\isanewline

\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}{\isacharparenright}\isanewline

\isanewline

\isacommand{code{\isacharunderscore}const}\isamarkupfalse%

\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline

\ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%

\endisatagquotett

{\isafoldquotett}%

%

\isadelimquotett

%

\endisadelimquotett

%

\begin{isamarkuptext}%

\noindent A problem now occurs whenever a type which

  is an instance of \isa{eq} in \isa{HOL} is mapped

  on a \isa{Haskell}-built-in type which is also an instance

  of \isa{Haskell} \isa{Eq}:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

\isacommand{typedecl}\isamarkupfalse%

\ bar\isanewline

\isanewline

\isacommand{instantiation}\isamarkupfalse%

\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline

\isakeyword{begin}\isanewline

\isanewline

\isacommand{definition}\isamarkupfalse%

\ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}x{\isasymColon}bar{\isacharparenright}\ y\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline

\isanewline

\isacommand{instance}\isamarkupfalse%

\ \isacommand{by}\isamarkupfalse%

\ default\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq{\isacharunderscore}bar{\isacharunderscore}def{\isacharparenright}\isanewline

\isanewline

\isacommand{end}\isamarkupfalse%

%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\isadelimquotett

\ %

\endisadelimquotett

%

\isatagquotett

\isacommand{code{\isacharunderscore}type}\isamarkupfalse%

\ bar\isanewline

\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}%

\endisatagquotett

{\isafoldquotett}%

%

\isadelimquotett

%

\endisadelimquotett

%

\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

  \isa{code{\isacharunderscore}instance}:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquotett

%

\endisadelimquotett

%

\isatagquotett

\isacommand{code{\isacharunderscore}instance}\isamarkupfalse%

\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline

\ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}%

\endisatagquotett

{\isafoldquotett}%

%

\isadelimquotett

%

\endisadelimquotett

%

\isamarkupsubsection{Enhancing the target language context \label{sec:include}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

In rare cases it is necessary to \emph{enrich} the context of a

  target language;  this is accomplished using the \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}

  command:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquotett

%

\endisadelimquotett

%

\isatagquotett

\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

%

\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 target language.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimtheory

%

\endisadelimtheory

%

\isatagtheory

\isacommand{end}\isamarkupfalse%

%

\endisatagtheory

{\isafoldtheory}%

%

\isadelimtheory

%

\endisadelimtheory

\isanewline

\end{isabellebody}%

%%% Local Variables:

%%% mode: latex

%%% TeX-master: "root"

%%% End: