src/Doc/Codegen/Adaptation.thy

 
   \begin{itemize}
     \item improving readability and aesthetics of generated code
     \item gaining efficiency
     \item interface with language parts which have no direct counterpart
-      in @{text "HOL"} (say, imperative data structures)
+      in \<open>HOL\<close> (say, imperative data structures)
   \end{itemize}
 
   \noindent Generally, you should avoid using those features yourself
   \emph{at any cost}:
 

     \item Subtle errors can be introduced unconsciously.
 
   \end{itemize}
 
   \noindent However, even if you ought refrain from setting up
-  adaptation yourself, already @{text "HOL"} comes with some
+  adaptation yourself, already \<open>HOL\<close> comes with some
   reasonable default adaptations (say, using target language list
   syntax).  There also some common adaptation 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.

     \caption{The adaptation principle}
     \label{fig:adaptation}
   \end{figure}
 
   \noindent In the tame view, code generation acts as broker between
-  @{text logic}, @{text "intermediate language"} and @{text "target
-  language"} by means of @{text translation} and @{text
-  serialisation}; for the latter, the serialiser has to observe the
-  structure of the @{text language} itself plus some @{text reserved}
+  \<open>logic\<close>, \<open>intermediate language\<close> and \<open>target
+  language\<close> by means of \<open>translation\<close> and \<open>serialisation\<close>; for the latter, the serialiser has to observe the
+  structure of the \<open>language\<close> itself plus some \<open>reserved\<close>
   keywords which have to be avoided for generated code.  However, if
-  you consider @{text adaptation} mechanisms, the code generated by
+  you consider \<open>adaptation\<close> mechanisms, the code generated by
   the serializer is just the tip of the iceberg:
 
   \begin{itemize}
 
-    \item @{text serialisation} can be \emph{parametrised} such that
+    \item \<open>serialisation\<close> can be \emph{parametrised} such that
       logical entities are mapped to target-specific ones
       (e.g. target-specific list syntax, see also
       \secref{sec:adaptation_mechanisms})
 
     \item Such parametrisations can involve references to a
-      target-specific standard @{text library} (e.g. using the @{text
-      Haskell} @{verbatim Maybe} type instead of the @{text HOL}
+      target-specific standard \<open>library\<close> (e.g. using the \<open>Haskell\<close> @{verbatim Maybe} type instead of the \<open>HOL\<close>
       @{type "option"} type); if such are used, the corresponding
       identifiers (in our example, @{verbatim Maybe}, @{verbatim
-      Nothing} and @{verbatim Just}) also have to be considered @{text
-      reserved}.
+      Nothing} and @{verbatim Just}) also have to be considered \<open>reserved\<close>.
 
     \item Even more, the user can enrich the library of the
-      target-language by providing code snippets (\qt{@{text
-      "includes"}}) which are prepended to any generated code (see
+      target-language by providing code snippets (\qt{\<open>includes\<close>}) which are prepended to any generated code (see
       \secref{sec:include}); this typically also involves further
-      @{text reserved} identifiers.
+      \<open>reserved\<close> identifiers.
 
   \end{itemize}
 
   \noindent As figure \ref{fig:adaptation} illustrates, all these
   adaptation mechanisms have to act consistently; it is at the

        types @{typ integer} and @{typ natural} isomorphic to types
        @{typ int} and @{typ nat} respectively.  Type @{typ integer}
        is mapped to target-language built-in integers; @{typ natural}
        is implemented as abstract type over @{typ integer}.
        Useful for code setups which involve e.g.~indexing
-       of target-language arrays.  Part of @{text "HOL-Main"}.
+       of target-language arrays.  Part of \<open>HOL-Main\<close>.
 
     \item[@{theory "HOL.String"}] provides an additional datatype @{typ
        String.literal} which is isomorphic to lists of 7-bit (ASCII) characters;
        @{typ String.literal}s are mapped to target-language strings.
 
        Literal values of type @{typ String.literal} can be written
-       as @{text "STR ''\<dots>''"} for sequences of printable characters and
-       @{text "STR 0x\<dots>"} for one single ASCII code point given
+       as \<open>STR ''\<dots>''\<close> for sequences of printable characters and
+       \<open>STR 0x\<dots>\<close> for one single ASCII code point given
        as hexadecimal numeral; @{typ String.literal} supports concatenation
-       @{text "\<dots> + \<dots>"} for all standard target languages.
+       \<open>\<dots> + \<dots>\<close> for all standard target languages.
 
        Note that the particular notion of \qt{string} is target-language
        specific (sequence of 8-bit units, sequence of unicode code points, \ldots);
        hence ASCII is the only reliable common base e.g.~for
        printing (error) messages; more sophisticated applications

        not contain non-ASCII-characters, to safeguard consistency.
        On top of these, more abstract conversions like @{term_type
        String.explode} and @{term_type String.implode}
        are implemented.
        
-       Part of @{text "HOL-Main"}.
-
-    \item[@{text "Code_Target_Int"}] implements type @{typ int}
+       Part of \<open>HOL-Main\<close>.
+
+    \item[\<open>Code_Target_Int\<close>] implements type @{typ int}
        by @{typ integer} and thus by target-language built-in integers.
 
-    \item[@{text "Code_Binary_Nat"}] implements type
+    \item[\<open>Code_Binary_Nat\<close>] implements type
        @{typ nat} using a binary rather than a linear representation,
        which yields a considerable speedup for computations.
        Pattern matching with @{term "0::nat"} / @{const "Suc"} is eliminated
        by a preprocessor.\label{abstract_nat}
 
-    \item[@{text "Code_Target_Nat"}] implements type @{typ nat}
+    \item[\<open>Code_Target_Nat\<close>] implements type @{typ nat}
        by @{typ integer} and thus by target-language built-in integers.
        Pattern matching with @{term "0::nat"} / @{const "Suc"} is eliminated
        by a preprocessor.
 
-    \item[@{text "Code_Target_Numeral"}] is a convenience theory
-       containing both @{text "Code_Target_Nat"} and
-       @{text "Code_Target_Int"}.
+    \item[\<open>Code_Target_Numeral\<close>] is a convenience theory
+       containing both \<open>Code_Target_Nat\<close> and
+       \<open>Code_Target_Int\<close>.
 
     \item[@{theory "HOL-Library.IArray"}] provides a type @{typ "'a iarray"}
        isomorphic to lists but implemented by (effectively immutable)
        arrays \emph{in SML only}.
 

   proper underscore while the second ``@{verbatim "_"}'' is a
   placeholder.
 \<close>
 
 
-subsection \<open>@{text Haskell} serialisation\<close>
-
-text \<open>
-  For convenience, the default @{text HOL} setup for @{text Haskell}
-  maps the @{class equal} class to its counterpart in @{text Haskell},
+subsection \<open>\<open>Haskell\<close> serialisation\<close>
+
+text \<open>
+  For convenience, the default \<open>HOL\<close> setup for \<open>Haskell\<close>
+  maps the @{class equal} class to its counterpart in \<open>Haskell\<close>,
   giving custom serialisations for the class @{class equal}
   and its operation @{const [source] HOL.equal}.
 \<close>
 
 code_printing %quotett
   type_class equal \<rightharpoonup> (Haskell) "Eq"
 | constant HOL.equal \<rightharpoonup> (Haskell) infixl 4 "=="
 
 text \<open>
   \noindent A problem now occurs whenever a type which is an instance
-  of @{class equal} in @{text HOL} is mapped on a @{text
-  Haskell}-built-in type which is also an instance of @{text Haskell}
-  @{text Eq}:
+  of @{class equal} in \<open>HOL\<close> is mapped on a \<open>Haskell\<close>-built-in type which is also an instance of \<open>Haskell\<close>
+  \<open>Eq\<close>:
 \<close>
 
 typedecl %quote bar
 
 instantiation %quote bar :: equal

 (*>*) code_printing %quotett
   type_constructor bar \<rightharpoonup> (Haskell) "Integer"
 
 text \<open>
   \noindent The code generator would produce an additional instance,
-  which of course is rejected by the @{text Haskell} compiler.  To
+  which of course is rejected by the \<open>Haskell\<close> compiler.  To
   suppress this additional instance:
 \<close>
 
 code_printing %quotett
   class_instance bar :: "HOL.equal" \<rightharpoonup> (Haskell) -