# HG changeset patch
# User haftmann
# Date 1421325581 -3600
# Node ID 056945909f60d6fc502630fad9465b5c98ceda29
# Parent  ead400fd6484637df0dcf1451762d0e4366cf152
modernized cartouches

diff -r ead400fd6484 -r 056945909f60 src/Doc/Codegen/Adaptation.thy
--- a/src/Doc/Codegen/Adaptation.thy	Thu Jan 15 13:39:41 2015 +0100
+++ b/src/Doc/Codegen/Adaptation.thy	Thu Jan 15 13:39:41 2015 +0100
@@ -2,14 +2,14 @@
 imports Setup
 begin
 
-setup %invisible {* Code_Target.add_derived_target ("\<SML>", [("SML", I)])
-  #> Code_Target.add_derived_target ("\<SMLdummy>", [("Haskell", I)]) *}
+setup %invisible \<open>Code_Target.add_derived_target ("\<SML>", [("SML", I)])
+  #> Code_Target.add_derived_target ("\<SMLdummy>", [("Haskell", I)])\<close>
 
-section {* Adaptation to target languages \label{sec:adaptation} *}
+section \<open>Adaptation to target languages \label{sec:adaptation}\<close>
 
-subsection {* Adapting code generation *}
+subsection \<open>Adapting code generation\<close>
 
-text {*
+text \<open>
   The aspects of code generation introduced so far have two aspects
   in common:
 
@@ -61,12 +61,12 @@
   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.
-*}
+\<close>
 
 
-subsection {* The adaptation principle *}
+subsection \<open>The adaptation principle\<close>
 
-text {*
+text \<open>
   Figure \ref{fig:adaptation} illustrates what \qt{adaptation} is
   conceptually supposed to be:
 
@@ -146,11 +146,11 @@
   \noindent As figure \ref{fig:adaptation} illustrates, all these
   adaptation mechanisms have to act consistently; it is at the
   discretion of the user to take care for this.
-*}
+\<close>
 
-subsection {* Common adaptation patterns *}
+subsection \<open>Common adaptation patterns\<close>
 
-text {*
+text \<open>
   The @{theory HOL} @{theory Main} theory already provides a code
   generator setup which should be suitable for most applications.
   Common extensions and modifications are available by certain
@@ -200,14 +200,14 @@
        arrays \emph{in SML only}.
 
   \end{description}
-*}
+\<close>
 
 
-subsection {* Parametrising serialisation \label{sec:adaptation_mechanisms} *}
+subsection \<open>Parametrising serialisation \label{sec:adaptation_mechanisms}\<close>
 
-text {*
+text \<open>
   Consider the following function and its corresponding SML code:
-*}
+\<close>
 
 primrec %quote in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
   "in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l"
@@ -219,11 +219,11 @@
 | constant HOL.conj \<rightharpoonup> (SML)
 | constant Not \<rightharpoonup> (SML)
 (*>*)
-text %quotetypewriter {*
+text %quotetypewriter \<open>
   @{code_stmts in_interval (SML)}
-*}
+\<close>
 
-text {*
+text \<open>
   \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
@@ -232,7 +232,7 @@
   which would perfectly terminate when the existing SML @{verbatim
   "bool"} would be used.  To map the HOL @{typ bool} on SML @{verbatim
   "bool"}, we may use \qn{custom serialisations}:
-*}
+\<close>
 
 code_printing %quotett
   type_constructor bool \<rightharpoonup> (SML) "bool"
@@ -240,7 +240,7 @@
 | constant False \<rightharpoonup> (SML) "false"
 | constant HOL.conj \<rightharpoonup> (SML) "_ andalso _"
 
-text {*
+text \<open>
   \noindent The @{command_def code_printing} command takes a series
   of symbols (contants, type constructor, \ldots)
   together with target-specific custom serialisations.  Each
@@ -249,28 +249,28 @@
   inserted whenever the type constructor would occur.  Each
   ``@{verbatim "_"}'' in a serialisation expression is treated as a
   placeholder for the constant's or the type constructor's arguments.
-*}
+\<close>
 
-text %quotetypewriter {*
+text %quotetypewriter \<open>
   @{code_stmts in_interval (SML)}
-*}
+\<close>
 
-text {*
+text \<open>
   \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:
-*}
+\<close>
 
 code_printing %quotett
   constant HOL.conj \<rightharpoonup> (SML) infixl 1 "andalso"
 
-text %quotetypewriter {*
+text %quotetypewriter \<open>
   @{code_stmts in_interval (SML)}
-*}
+\<close>
 
-text {*
+text \<open>
   \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
@@ -278,14 +278,14 @@
   typically contains the keywords of the target language.  It can be
   extended manually, thus avoiding accidental overwrites, using the
   @{command_def "code_reserved"} command:
-*}
+\<close>
 
 code_reserved %quote "\<SMLdummy>" bool true false andalso
 
-text {*
+text \<open>
   \noindent Next, we try to map HOL pairs to SML pairs, using the
   infix ``@{verbatim "*"}'' type constructor and parentheses:
-*}
+\<close>
 (*<*)
 code_printing %invisible
   type_constructor prod \<rightharpoonup> (SML)
@@ -295,7 +295,7 @@
   type_constructor prod \<rightharpoonup> (SML) infix 2 "*"
 | constant Pair \<rightharpoonup> (SML) "!((_),/ (_))"
 
-text {*
+text \<open>
   \noindent The initial bang ``@{verbatim "!"}'' tells the serialiser
   never to put parentheses around the whole expression (they are
   already present), while the parentheses around argument place
@@ -314,28 +314,28 @@
   in ``@{verbatim "fn '_ => _"}'' the first ``@{verbatim "_"}'' is a
   proper underscore while the second ``@{verbatim "_"}'' is a
   placeholder.
-*}
+\<close>
 
 
-subsection {* @{text Haskell} serialisation *}
+subsection \<open>@{text Haskell} serialisation\<close>
 
-text {*
+text \<open>
   For convenience, the default @{text HOL} setup for @{text Haskell}
   maps the @{class equal} class to its counterpart in @{text Haskell},
   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 {*
+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}:
-*}
+\<close>
 
 typedecl %quote bar
 
@@ -351,35 +351,35 @@
 (*>*) code_printing %quotett
   type_constructor bar \<rightharpoonup> (Haskell) "Integer"
 
-text {*
+text \<open>
   \noindent The code generator would produce an additional instance,
   which of course is rejected by the @{text Haskell} compiler.  To
   suppress this additional instance:
-*}
+\<close>
 
 code_printing %quotett
   class_instance bar :: "HOL.equal" \<rightharpoonup> (Haskell) -
 
 
-subsection {* Enhancing the target language context \label{sec:include} *}
+subsection \<open>Enhancing the target language context \label{sec:include}\<close>
 
-text {*
+text \<open>
   In rare cases it is necessary to \emph{enrich} the context of a
   target language; this can also be accomplished using the @{command
   "code_printing"} command:
-*}
+\<close>
 
 code_printing %quotett
-  code_module "Errno" \<rightharpoonup> (Haskell) {*errno i = error ("Error number: " ++ show i)*}
+  code_module "Errno" \<rightharpoonup> (Haskell) \<open>errno i = error ("Error number: " ++ show i)\<close>
 
 code_reserved %quotett Haskell Errno
 
-text {*
+text \<open>
   \noindent Such named modules are then prepended to every
   generated code.  Inspect such code in order to find out how
   this behaves with respect to a particular
   target language.
-*}
+\<close>
 
 end
 
diff -r ead400fd6484 -r 056945909f60 src/Doc/Codegen/Evaluation.thy
--- a/src/Doc/Codegen/Evaluation.thy	Thu Jan 15 13:39:41 2015 +0100
+++ b/src/Doc/Codegen/Evaluation.thy	Thu Jan 15 13:39:41 2015 +0100
@@ -2,9 +2,9 @@
 imports Setup
 begin
 
-section {* Evaluation \label{sec:evaluation} *}
+section \<open>Evaluation \label{sec:evaluation}\<close>
 
-text {*
+text \<open>
   Recalling \secref{sec:principle}, code generation turns a system of
   equations into a program with the \emph{same} equational semantics.
   As a consequence, this program can be used as a \emph{rewrite
@@ -12,12 +12,12 @@
   term @{term "t'"} yields the theorems @{prop "t \<equiv> t'"}.  This
   application of code generation in the following is referred to as
   \emph{evaluation}.
-*}
+\<close>
 
 
-subsection {* Evaluation techniques *}
+subsection \<open>Evaluation techniques\<close>
 
-text {*
+text \<open>
   The existing infrastructure provides a rich palette of evaluation
   techniques, each comprising different aspects:
 
@@ -35,34 +35,34 @@
       trustable.
 
   \end{description}
-*}
+\<close>
 
 
-subsubsection {* The simplifier (@{text simp}) *}
+subsubsection \<open>The simplifier (@{text simp})\<close>
 
-text {*
+text \<open>
   The simplest way for evaluation is just using the simplifier with
   the original code equations of the underlying program.  This gives
   fully symbolic evaluation and highest trustablity, with the usual
   performance of the simplifier.  Note that for operations on abstract
   datatypes (cf.~\secref{sec:invariant}), the original theorems as
   given by the users are used, not the modified ones.
-*}
+\<close>
 
 
-subsubsection {* Normalization by evaluation (@{text nbe}) *}
+subsubsection \<open>Normalization by evaluation (@{text nbe})\<close>
 
-text {*
+text \<open>
   Normalization by evaluation @{cite "Aehlig-Haftmann-Nipkow:2008:nbe"}
   provides a comparably fast partially symbolic evaluation which
   permits also normalization of functions and uninterpreted symbols;
   the stack of code to be trusted is considerable.
-*}
+\<close>
 
 
-subsubsection {* Evaluation in ML (@{text code}) *}
+subsubsection \<open>Evaluation in ML (@{text code})\<close>
 
-text {*
+text \<open>
   Highest performance can be achieved by evaluation in ML, at the cost
   of being restricted to ground results and a layered stack of code to
   be trusted, including code generator configurations by the user.
@@ -73,32 +73,32 @@
   out there depends crucially on the correctness of the code
   generator setup; this is one of the reasons why you should not use
   adaptation (see \secref{sec:adaptation}) frivolously.
-*}
+\<close>
 
 
-subsection {* Aspects of evaluation *}
+subsection \<open>Aspects of evaluation\<close>
 
-text {*
+text \<open>
   Each of the techniques can be combined with different aspects.  The
   most important distinction is between dynamic and static evaluation.
   Dynamic evaluation takes the code generator configuration \qt{as it
   is} at the point where evaluation is issued.  Best example is the
   @{command_def value} command which allows ad-hoc evaluation of
   terms:
-*}
+\<close>
 
 value %quote "42 / (12 :: rat)"
 
-text {*
+text \<open>
   \noindent @{command value} tries first to evaluate using ML, falling
   back to normalization by evaluation if this fails.
 
   A particular technique may be specified in square brackets, e.g.
-*}
+\<close>
 
 value %quote [nbe] "42 / (12 :: rat)"
 
-text {*
+text \<open>
   To employ dynamic evaluation in the document generation, there is also
   a @{text value} antiquotation with the same evaluation techniques 
   as @{command value}.
@@ -162,12 +162,12 @@
   For property conversion (which coincides with conversion except for
   evaluation in ML), methods are provided which solve a given goal by
   evaluation.
-*}
+\<close>
 
 
-subsection {* Schematic overview *}
+subsection \<open>Schematic overview\<close>
 
-text {*
+text \<open>
   \newcommand{\ttsize}{\fontsize{5.8pt}{8pt}\selectfont}
   \fontsize{9pt}{12pt}\selectfont
   \begin{tabular}{ll||c|c|c}
@@ -189,12 +189,12 @@
       & \ttsize@{ML "Nbe.static_conv"}
       & \ttsize@{ML "Code_Evaluation.static_conv"}
   \end{tabular}
-*}
+\<close>
 
 
-subsection {* Preprocessing HOL terms into evaluable shape *}
+subsection \<open>Preprocessing HOL terms into evaluable shape\<close>
 
-text {*
+text \<open>
   When integration decision procedures developed inside HOL into HOL itself,
   it is necessary to somehow get from the Isabelle/ML representation to
   the representation used by the decision procedure itself (``reification'').
@@ -203,7 +203,7 @@
   @{ML "Reification.conv"} and @{ML "Reification.tac"}
 
   An simplistic example:
-*}
+\<close>
 
 datatype %quote form_ord = T | F | Less nat nat
   | And form_ord form_ord | Or form_ord form_ord | Neg form_ord
@@ -217,21 +217,21 @@
 | "interp (Or f1 f2) vs \<longleftrightarrow> interp f1 vs \<or> interp f2 vs"
 | "interp (Neg f) vs \<longleftrightarrow> \<not> interp f vs"
 
-text {*
+text \<open>
   The datatype @{type form_ord} represents formulae whose semantics is given by
   @{const interp}.  Note that values are represented by variable indices (@{typ nat})
   whose concrete values are given in list @{term vs}.
-*}
+\<close>
 
-ML (*<*) {* *}
+ML (*<*) \<open>\<close>
 schematic_lemma "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> ?P"
 ML_prf 
-(*>*) {* val thm =
-  Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"} *} (*<*)
-by (tactic {* ALLGOALS (rtac thm) *})
+(*>*) \<open>val thm =
+  Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"}\<close> (*<*)
+by (tactic \<open>ALLGOALS (rtac thm)\<close>)
 (*>*) 
 
-text {*
+text \<open>
   By virtue of @{fact interp.simps}, @{ML "Reification.conv"} provides a conversion
   which, for this concrete example, yields @{thm thm [no_vars]}.  Note that the argument
   to @{const interp} does not contain any free variables and can thus be evaluated
@@ -239,38 +239,38 @@
 
   A less meager example can be found in the AFP, session @{text "Regular-Sets"},
   theory @{text Regexp_Method}.
-*}
+\<close>
 
 
-subsection {* Intimate connection between logic and system runtime *}
+subsection \<open>Intimate connection between logic and system runtime\<close>
 
-text {*
+text \<open>
   The toolbox of static evaluation conversions forms a reasonable base
   to interweave generated code and system tools.  However in some
   situations more direct interaction is desirable.
-*}
+\<close>
 
 
-subsubsection {* Static embedding of generated code into system runtime -- the @{text code} antiquotation \label{sec:code_antiq} *}
+subsubsection \<open>Static embedding of generated code into system runtime -- the @{text code} antiquotation \label{sec:code_antiq}\<close>
 
-text {*
+text \<open>
   The @{text code} antiquotation allows to include constants from
   generated code directly into ML system code, as in the following toy
   example:
-*}
+\<close>
 
 datatype %quote form = T | F | And form form | Or form form (*<*)
 
-(*>*) ML %quotett {*
+(*>*) ML %quotett \<open>
   fun eval_form @{code T} = true
     | eval_form @{code F} = false
     | eval_form (@{code And} (p, q)) =
         eval_form p andalso eval_form q
     | eval_form (@{code Or} (p, q)) =
         eval_form p orelse eval_form q;
-*}
+\<close>
 
-text {*
+text \<open>
   \noindent @{text code} takes as argument the name of a constant;
   after the whole ML is read, the necessary code is generated
   transparently and the corresponding constant names are inserted.
@@ -281,24 +281,24 @@
 
   For a less simplistic example, theory @{text Approximation} in
   the @{text Decision_Procs} session is a good reference.
-*}
+\<close>
 
 
-subsubsection {* Static embedding of generated code into system runtime -- @{text code_reflect} *}
+subsubsection \<open>Static embedding of generated code into system runtime -- @{text code_reflect}\<close>
 
-text {*
+text \<open>
   The @{text code} antiquoation is lightweight, but the generated code
   is only accessible while the ML section is processed.  Sometimes this
   is not appropriate, especially if the generated code contains datatype
   declarations which are shared with other parts of the system.  In these
   cases, @{command_def code_reflect} can be used:
-*}
+\<close>
 
 code_reflect %quote Sum_Type
   datatypes sum = Inl | Inr
   functions "Sum_Type.sum.projl" "Sum_Type.sum.projr"
 
-text {*
+text \<open>
   \noindent @{command_def code_reflect} takes a structure name and
   references to datatypes and functions; for these code is compiled
   into the named ML structure and the \emph{Eval} target is modified
@@ -309,17 +309,17 @@
 
   A typical example for @{command code_reflect} can be found in the
   @{theory Predicate} theory.
-*}
+\<close>
 
 
-subsubsection {* Separate compilation -- @{text code_reflect} *}
+subsubsection \<open>Separate compilation -- @{text code_reflect}\<close>
 
-text {*
+text \<open>
   For technical reasons it is sometimes necessary to separate
   generation and compilation of code which is supposed to be used in
   the system runtime.  For this @{command code_reflect} with an
   optional @{text "file"} argument can be used:
-*}
+\<close>
 
 code_reflect %quote Rat
   datatypes rat = Frct
@@ -328,10 +328,10 @@
     "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)"
   file "$ISABELLE_TMP/examples/rat.ML"
 
-text {*
+text \<open>
   \noindent This merely generates the referenced code to the given
   file which can be included into the system runtime later on.
-*}
+\<close>
 
 end
 
diff -r ead400fd6484 -r 056945909f60 src/Doc/Codegen/Foundations.thy
--- a/src/Doc/Codegen/Foundations.thy	Thu Jan 15 13:39:41 2015 +0100
+++ b/src/Doc/Codegen/Foundations.thy	Thu Jan 15 13:39:41 2015 +0100
@@ -2,11 +2,11 @@
 imports Introduction
 begin
 
-section {* Code generation foundations \label{sec:foundations} *}
+section \<open>Code generation foundations \label{sec:foundations}\<close>
 
-subsection {* Code generator architecture \label{sec:architecture} *}
+subsection \<open>Code generator architecture \label{sec:architecture}\<close>
 
-text {*
+text \<open>
   The code generator is actually a framework consisting of different
   components which can be customised individually.
 
@@ -90,12 +90,12 @@
   \noindent From these steps, only the last two are carried out
   outside the logic; by keeping this layer as thin as possible, the
   amount of code to trust is kept to a minimum.
-*}
+\<close>
 
 
-subsection {* The pre- and postprocessor \label{sec:preproc} *}
+subsection \<open>The pre- and postprocessor \label{sec:preproc}\<close>
 
-text {*
+text \<open>
   Before selected function theorems are turned into abstract code, a
   chain of definitional transformation steps is carried out:
   \emph{preprocessing}.  The preprocessor consists of two
@@ -122,13 +122,13 @@
   is is just expressed as @{term "x \<in> set xs"}.  But for execution
   the intermediate set is not desirable.  Hence the following
   specification:
-*}
+\<close>
 
 definition %quote member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool"
 where
   [code_abbrev]: "member xs x \<longleftrightarrow> x \<in> set xs"
 
-text {*
+text \<open>
   \noindent The \emph{@{attribute code_abbrev} attribute} declares
   its theorem a rewrite rule for the postprocessor and the symmetric
   of its theorem as rewrite rule for the preprocessor.  Together,
@@ -153,12 +153,12 @@
   code_thms} (see \secref{sec:equations}) provides a convenient
   mechanism to inspect the impact of a preprocessor setup on code
   equations.
-*}
+\<close>
 
 
-subsection {* Understanding code equations \label{sec:equations} *}
+subsection \<open>Understanding code equations \label{sec:equations}\<close>
 
-text {*
+text \<open>
   As told in \secref{sec:principle}, the notion of code equations is
   vital to code generation.  Indeed most problems which occur in
   practice can be resolved by an inspection of the underlying code
@@ -166,7 +166,7 @@
 
   It is possible to exchange the default code equations for constants
   by explicitly proving alternative ones:
-*}
+\<close>
 
 lemma %quote [code]:
   "dequeue (AQueue xs []) =
@@ -176,18 +176,18 @@
      (Some y, AQueue xs ys)"
   by (cases xs, simp_all) (cases "rev xs", simp_all)
 
-text {*
+text \<open>
   \noindent The annotation @{text "[code]"} is an @{text attribute}
   which states that the given theorems should be considered as code
   equations for a @{text fun} statement -- the corresponding constant
   is determined syntactically.  The resulting code:
-*}
+\<close>
 
-text %quotetypewriter {*
+text %quotetypewriter \<open>
   @{code_stmts dequeue (consts) dequeue (Haskell)}
-*}
+\<close>
 
-text {*
+text \<open>
   \noindent You may note that the equality test @{term "xs = []"} has
   been replaced by the predicate @{term "List.null xs"}.  This is due
   to the default setup of the \qn{preprocessor}.
@@ -206,24 +206,24 @@
   The code equations after preprocessing are already are blueprint of
   the generated program and can be inspected using the @{command
   code_thms} command:
-*}
+\<close>
 
 code_thms %quote dequeue
 
-text {*
+text \<open>
   \noindent This prints a table with the code equations for @{const
   dequeue}, including \emph{all} code equations those equations depend
   on recursively.  These dependencies themselves can be visualized using
   the @{command_def code_deps} command.
-*}
+\<close>
 
 
-subsection {* Equality *}
+subsection \<open>Equality\<close>
 
-text {*
+text \<open>
   Implementation of equality deserves some attention.  Here an example
   function involving polymorphic equality:
-*}
+\<close>
 
 primrec %quote collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   "collect_duplicates xs ys [] = xs"
@@ -233,17 +233,17 @@
       else collect_duplicates xs (z#ys) zs
     else collect_duplicates (z#xs) (z#ys) zs)"
 
-text {*
+text \<open>
   \noindent During preprocessing, the membership test is rewritten,
   resulting in @{const List.member}, which itself performs an explicit
   equality check, as can be seen in the corresponding @{text SML} code:
-*}
+\<close>
 
-text %quotetypewriter {*
+text %quotetypewriter \<open>
   @{code_stmts collect_duplicates (SML)}
-*}
+\<close>
 
-text {*
+text \<open>
   \noindent Obviously, polymorphic equality is implemented the Haskell
   way using a type class.  How is this achieved?  HOL introduces an
   explicit class @{class equal} with a corresponding operation @{const
@@ -252,15 +252,15 @@
   through all dependent code equations.  For datatypes, instances of
   @{class equal} are implicitly derived when possible.  For other types,
   you may instantiate @{text equal} manually like any other type class.
-*}
+\<close>
 
 
-subsection {* Explicit partiality \label{sec:partiality} *}
+subsection \<open>Explicit partiality \label{sec:partiality}\<close>
 
-text {*
+text \<open>
   Partiality usually enters the game by partial patterns, as
   in the following example, again for amortised queues:
-*}
+\<close>
 
 definition %quote strict_dequeue :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
   "strict_dequeue q = (case dequeue q
@@ -272,19 +272,19 @@
     (case rev xs of y # ys \<Rightarrow> (y, AQueue [] ys))"
   by (simp_all add: strict_dequeue_def) (cases xs, simp_all split: list.split)
 
-text {*
+text \<open>
   \noindent In the corresponding code, there is no equation
   for the pattern @{term "AQueue [] []"}:
-*}
+\<close>
 
-text %quotetypewriter {*
+text %quotetypewriter \<open>
   @{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}
-*}
+\<close>
 
-text {*
+text \<open>
   \noindent In some cases it is desirable to have this
   pseudo-\qt{partiality} more explicitly, e.g.~as follows:
-*}
+\<close>
 
 axiomatization %quote empty_queue :: 'a
 
@@ -298,7 +298,7 @@
      (y, AQueue xs ys)"
   by (simp_all add: strict_dequeue'_def split: list.splits)
 
-text {*
+text \<open>
   Observe that on the right hand side of the definition of @{const
   "strict_dequeue'"}, the unspecified constant @{const empty_queue} occurs.
 
@@ -310,30 +310,30 @@
   side.  In order to categorise a constant into that category
   explicitly, use the @{attribute code} attribute with
   @{text abort}:
-*}
+\<close>
 
 declare %quote [[code abort: empty_queue]]
 
-text {*
+text \<open>
   \noindent Then the code generator will just insert an error or
   exception at the appropriate position:
-*}
+\<close>
 
-text %quotetypewriter {*
+text %quotetypewriter \<open>
   @{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}
-*}
+\<close>
 
-text {*
+text \<open>
   \noindent This feature however is rarely needed in practice.  Note
   also that the HOL default setup already declares @{const undefined},
   which is most likely to be used in such situations, as
   @{text "code abort"}.
-*}
+\<close>
 
 
-subsection {* If something goes utterly wrong \label{sec:utterly_wrong} *}
+subsection \<open>If something goes utterly wrong \label{sec:utterly_wrong}\<close>
 
-text {*
+text \<open>
   Under certain circumstances, the code generator fails to produce
   code entirely.  To debug these, the following hints may prove
   helpful:
@@ -371,6 +371,6 @@
       class signatures (\qt{wellsortedness error}).
 
   \end{description}
-*}
+\<close>
 
 end
diff -r ead400fd6484 -r 056945909f60 src/Doc/Codegen/Further.thy
--- a/src/Doc/Codegen/Further.thy	Thu Jan 15 13:39:41 2015 +0100
+++ b/src/Doc/Codegen/Further.thy	Thu Jan 15 13:39:41 2015 +0100
@@ -2,11 +2,11 @@
 imports Setup "~~/src/Tools/Permanent_Interpretation"
 begin
 
-section {* Further issues \label{sec:further} *}
+section \<open>Further issues \label{sec:further}\<close>
 
-subsection {* Specialities of the @{text Scala} target language \label{sec:scala} *}
+subsection \<open>Specialities of the @{text Scala} target language \label{sec:scala}\<close>
 
-text {*
+text \<open>
   @{text Scala} deviates from languages of the ML family in a couple
   of aspects; those which affect code generation mainly have to do with
   @{text Scala}'s type system:
@@ -43,7 +43,7 @@
   Isabelle's type classes are mapped onto @{text Scala} implicits; in
   cases with diamonds in the subclass hierarchy this can lead to
   ambiguities in the generated code:
-*}
+\<close>
 
 class %quote class1 =
   fixes foo :: "'a \<Rightarrow> 'a"
@@ -52,62 +52,62 @@
 
 class %quote class3 = class1
 
-text {*
+text \<open>
   \noindent Here both @{class class2} and @{class class3} inherit from @{class class1},
   forming the upper part of a diamond.
-*}
+\<close>
 
 definition %quote bar :: "'a :: {class2, class3} \<Rightarrow> 'a" where
   "bar = foo"
 
-text {*
+text \<open>
   \noindent This yields the following code:
-*}
+\<close>
 
-text %quotetypewriter {*
+text %quotetypewriter \<open>
   @{code_stmts bar (Scala)}
-*}
+\<close>
 
-text {*
+text \<open>
   \noindent This code is rejected by the @{text Scala} compiler: in
   the definition of @{text bar}, it is not clear from where to derive
   the implicit argument for @{text foo}.
 
   The solution to the problem is to close the diamond by a further
   class with inherits from both @{class class2} and @{class class3}:
-*}
+\<close>
 
 class %quote class4 = class2 + class3
 
-text {*
+text \<open>
   \noindent Then the offending code equation can be restricted to
   @{class class4}:
-*}
+\<close>
 
 lemma %quote [code]:
   "(bar :: 'a::class4 \<Rightarrow> 'a) = foo"
   by (simp only: bar_def)
 
-text {*
+text \<open>
   \noindent with the following code:
-*}
+\<close>
 
-text %quotetypewriter {*
+text %quotetypewriter \<open>
   @{code_stmts bar (Scala)}
-*}
+\<close>
 
-text {*
+text \<open>
   \noindent which exposes no ambiguity.
 
   Since the preprocessor (cf.~\secref{sec:preproc}) propagates sort
   constraints through a system of code equations, it is usually not
   very difficult to identify the set of code equations which actually
   needs more restricted sort constraints.
-*}
+\<close>
 
-subsection {* Modules namespace *}
+subsection \<open>Modules namespace\<close>
 
-text {*
+text \<open>
   When invoking the @{command export_code} command it is possible to
   leave out the @{keyword "module_name"} part; then code is
   distributed over different modules, where the module name space
@@ -122,38 +122,38 @@
   A solution is to declare module names explicitly.  Let use assume
   the three cyclically dependent modules are named \emph{A}, \emph{B}
   and \emph{C}.  Then, by stating
-*}
+\<close>
 
 code_identifier %quote
   code_module A \<rightharpoonup> (SML) ABC
 | code_module B \<rightharpoonup> (SML) ABC
 | code_module C \<rightharpoonup> (SML) ABC
 
-text {*
+text \<open>
   \noindent we explicitly map all those modules on \emph{ABC},
   resulting in an ad-hoc merge of this three modules at serialisation
   time.
-*}
+\<close>
 
-subsection {* Locales and interpretation *}
+subsection \<open>Locales and interpretation\<close>
 
-text {*
+text \<open>
   A technical issue comes to surface when generating code from
   specifications stemming from locale interpretation.
 
   Let us assume a locale specifying a power operation on arbitrary
   types:
-*}
+\<close>
 
 locale %quote power =
   fixes power :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
   assumes power_commute: "power x \<circ> power y = power y \<circ> power x"
 begin
 
-text {*
+text \<open>
   \noindent Inside that locale we can lift @{text power} to exponent
   lists by means of specification relative to that locale:
-*}
+\<close>
 
 primrec %quote powers :: "'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
   "powers [] = id"
@@ -175,7 +175,7 @@
 
 end %quote
 
-text {*
+text \<open>
   After an interpretation of this locale (say, @{command_def
   interpretation} @{text "fun_power:"} @{term [source] "power (\<lambda>n (f
   :: 'a \<Rightarrow> 'a). f ^^ n)"}), one would expect to have a constant @{text
@@ -189,43 +189,43 @@
   achieved.  First, a dedicated definition of the constant on which
   the local @{text "powers"} after interpretation is supposed to be
   mapped on:
-*}
+\<close>
 
 definition %quote funpows :: "nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
   [code del]: "funpows = power.powers (\<lambda>n f. f ^^ n)"
 
-text {*
+text \<open>
   \noindent In general, the pattern is @{text "c = t"} where @{text c}
   is the name of the future constant and @{text t} the foundational
   term corresponding to the local constant after interpretation.
 
   The interpretation itself is enriched with an equation @{text "t = c"}:
-*}
+\<close>
 
 interpretation %quote fun_power: power "(\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)" where
   "power.powers (\<lambda>n f. f ^^ n) = funpows"
   by unfold_locales
     (simp_all add: fun_eq_iff funpow_mult mult.commute funpows_def)
 
-text {*
+text \<open>
   \noindent This additional equation is trivially proved by the
   definition itself.
 
   After this setup procedure, code generation can continue as usual:
-*}
+\<close>
 
-text %quotetypewriter {*
+text %quotetypewriter \<open>
   @{code_stmts funpows (consts) Nat.funpow funpows (Haskell)}
-*} (*<*)
+\<close> (*<*)
 
-(*>*) text {*
+(*>*) text \<open>
   Fortunately, an even more succint approach is available using command
   @{command permanent_interpretation}.  This is available
   by importing theory @{file "~~/src/Tools/Permanent_Interpretation.thy"}.
   Then the pattern above collapses to
-*} (*<*)
+\<close> (*<*)
 
-setup {* Sign.add_path "funpows" *}
+setup \<open>Sign.add_path "funpows"\<close>
 hide_const (open) funpows
 
 (*>*)
@@ -234,43 +234,43 @@
   by unfold_locales
     (simp_all add: fun_eq_iff funpow_mult mult.commute) (*<*)
 
-setup {* Sign.parent_path *}
+setup \<open>Sign.parent_path\<close>
 
 (*>*)
 
 
-subsection {* Parallel computation *}
+subsection \<open>Parallel computation\<close>
 
-text {*
+text \<open>
   Theory @{text Parallel} in @{file "~~/src/HOL/Library"} contains
   operations to exploit parallelism inside the Isabelle/ML
   runtime engine.
-*}
+\<close>
 
-subsection {* Imperative data structures *}
+subsection \<open>Imperative data structures\<close>
 
-text {*
+text \<open>
   If you consider imperative data structures as inevitable for a
   specific application, you should consider \emph{Imperative
   Functional Programming with Isabelle/HOL}
   @{cite "bulwahn-et-al:2008:imperative"}; the framework described there
   is available in session @{text Imperative_HOL}, together with a
   short primer document.
-*}
+\<close>
 
 
-subsection {* ML system interfaces \label{sec:ml} *}
+subsection \<open>ML system interfaces \label{sec:ml}\<close>
 
-text {*
+text \<open>
   Since the code generator framework not only aims to provide a nice
   Isar interface but also to form a base for code-generation-based
   applications, here a short description of the most fundamental ML
   interfaces.
-*}
+\<close>
 
-subsubsection {* Managing executable content *}
+subsubsection \<open>Managing executable content\<close>
 
-text %mlref {*
+text %mlref \<open>
   \begin{mldecls}
   @{index_ML Code.read_const: "theory -> string -> string"} \\
   @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\
@@ -322,12 +322,12 @@
      if @{text const} is no constructor.
 
   \end{description}
-*}
+\<close>
 
 
-subsubsection {* Data depending on the theory's executable content *}
+subsubsection \<open>Data depending on the theory's executable content\<close>
 
-text {*
+text \<open>
   Implementing code generator applications on top of the framework set
   out so far usually not only involves using those primitive
   interfaces but also storing code-dependent data and various other
@@ -373,7 +373,7 @@
   \item @{text change_yield} update with side result.
 
   \end{description}
-*}
+\<close>
 
 end
 
diff -r ead400fd6484 -r 056945909f60 src/Doc/Codegen/Inductive_Predicate.thy
--- a/src/Doc/Codegen/Inductive_Predicate.thy	Thu Jan 15 13:39:41 2015 +0100
+++ b/src/Doc/Codegen/Inductive_Predicate.thy	Thu Jan 15 13:39:41 2015 +0100
@@ -16,9 +16,9 @@
   lexordp_def [unfolded lexord_def mem_Collect_eq split]
 (*>*)
 
-section {* Inductive Predicates \label{sec:inductive} *}
+section \<open>Inductive Predicates \label{sec:inductive}\<close>
 
-text {*
+text \<open>
   The @{text "predicate compiler"} is an extension of the code generator
   which turns inductive specifications into equational ones, from
   which in turn executable code can be generated.  The mechanisms of
@@ -27,20 +27,20 @@
 
   Consider the simple predicate @{const append} given by these two
   introduction rules:
-*}
+\<close>
 
-text %quote {*
+text %quote \<open>
   @{thm append.intros(1)[of ys]} \\
   @{thm append.intros(2)[of xs ys zs x]}
-*}
+\<close>
 
-text {*
+text \<open>
   \noindent To invoke the compiler, simply use @{command_def "code_pred"}:
-*}
+\<close>
 
 code_pred %quote append .
 
-text {*
+text \<open>
   \noindent The @{command "code_pred"} command takes the name of the
   inductive predicate and then you put a period to discharge a trivial
   correctness proof.  The compiler infers possible modes for the
@@ -56,55 +56,55 @@
     \item @{text "o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool"}
   \end{itemize}
   You can compute sets of predicates using @{command_def "values"}:
-*}
+\<close>
 
 values %quote "{zs. append [(1::nat),2,3] [4,5] zs}"
 
-text {* \noindent outputs @{text "{[1, 2, 3, 4, 5]}"}, and *}
+text \<open>\noindent outputs @{text "{[1, 2, 3, 4, 5]}"}, and\<close>
 
 values %quote "{(xs, ys). append xs ys [(2::nat),3]}"
 
-text {* \noindent outputs @{text "{([], [2, 3]), ([2], [3]), ([2, 3], [])}"}. *}
+text \<open>\noindent outputs @{text "{([], [2, 3]), ([2], [3]), ([2, 3], [])}"}.\<close>
 
-text {*
+text \<open>
   \noindent If you are only interested in the first elements of the
   set comprehension (with respect to a depth-first search on the
   introduction rules), you can pass an argument to @{command "values"}
   to specify the number of elements you want:
-*}
+\<close>
 
 values %quote 1 "{(xs, ys). append xs ys [(1::nat), 2, 3, 4]}"
 values %quote 3 "{(xs, ys). append xs ys [(1::nat), 2, 3, 4]}"
 
-text {*
+text \<open>
   \noindent The @{command "values"} command can only compute set
   comprehensions for which a mode has been inferred.
 
   The code equations for a predicate are made available as theorems with
   the suffix @{text "equation"}, and can be inspected with:
-*}
+\<close>
 
 thm %quote append.equation
 
-text {*
+text \<open>
   \noindent More advanced options are described in the following subsections.
-*}
+\<close>
 
-subsection {* Alternative names for functions *}
+subsection \<open>Alternative names for functions\<close>
 
-text {* 
+text \<open>
   By default, the functions generated from a predicate are named after
   the predicate with the mode mangled into the name (e.g., @{text
   "append_i_i_o"}).  You can specify your own names as follows:
-*}
+\<close>
 
 code_pred %quote (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool as concat,
   o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as split,
   i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix) append .
 
-subsection {* Alternative introduction rules *}
+subsection \<open>Alternative introduction rules\<close>
 
-text {*
+text \<open>
   Sometimes the introduction rules of an predicate are not executable
   because they contain non-executable constants or specific modes
   could not be inferred.  It is also possible that the introduction
@@ -113,34 +113,34 @@
   introduction rules for predicates with the attribute @{attribute
   "code_pred_intro"}.  For example, the transitive closure is defined
   by:
-*}
+\<close>
 
-text %quote {*
+text %quote \<open>
   @{lemma [source] "r a b \<Longrightarrow> tranclp r a b" by (fact tranclp.intros(1))}\\
   @{lemma [source] "tranclp r a b \<Longrightarrow> r b c \<Longrightarrow> tranclp r a c" by (fact tranclp.intros(2))}
-*}
+\<close>
 
-text {*
+text \<open>
   \noindent These rules do not suit well for executing the transitive
   closure with the mode @{text "(i \<Rightarrow> o \<Rightarrow> bool) \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}, as
   the second rule will cause an infinite loop in the recursive call.
   This can be avoided using the following alternative rules which are
   declared to the predicate compiler by the attribute @{attribute
   "code_pred_intro"}:
-*}
+\<close>
 
 lemma %quote [code_pred_intro]:
   "r a b \<Longrightarrow> tranclp r a b"
   "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
 by auto
 
-text {*
+text \<open>
   \noindent After declaring all alternative rules for the transitive
   closure, you invoke @{command "code_pred"} as usual.  As you have
   declared alternative rules for the predicate, you are urged to prove
   that these introduction rules are complete, i.e., that you can
   derive an elimination rule for the alternative rules:
-*}
+\<close>
 
 code_pred %quote tranclp
 proof -
@@ -148,20 +148,20 @@
   from this converse_tranclpE [OF tranclp.prems] show thesis by metis
 qed
 
-text {*
+text \<open>
   \noindent Alternative rules can also be used for constants that have
   not been defined inductively. For example, the lexicographic order
   which is defined as:
-*}
+\<close>
 
-text %quote {*
+text %quote \<open>
   @{thm [display] lexordp_def [of r]}
-*}
+\<close>
 
-text {*
+text \<open>
   \noindent To make it executable, you can derive the following two
   rules and prove the elimination rule:
-*}
+\<close>
 
 lemma %quote [code_pred_intro]:
   "append xs (a # v) ys \<Longrightarrow> lexordp r xs ys"
@@ -197,16 +197,16 @@
 qed(*>*)
 
 
-subsection {* Options for values *}
+subsection \<open>Options for values\<close>
 
-text {*
+text \<open>
   In the presence of higher-order predicates, multiple modes for some
   predicate could be inferred that are not disambiguated by the
   pattern of the set comprehension.  To disambiguate the modes for the
   arguments of a predicate, you can state the modes explicitly in the
   @{command "values"} command.  Consider the simple predicate @{term
   "succ"}:
-*}
+\<close>
 
 inductive %quote succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
   "succ 0 (Suc 0)"
@@ -214,7 +214,7 @@
 
 code_pred %quote succ .
 
-text {*
+text \<open>
   \noindent For this, the predicate compiler can infer modes @{text "o
   \<Rightarrow> o \<Rightarrow> bool"}, @{text "i \<Rightarrow> o \<Rightarrow> bool"}, @{text "o \<Rightarrow> i \<Rightarrow> bool"} and
   @{text "i \<Rightarrow> i \<Rightarrow> bool"}.  The invocation of @{command "values"}
@@ -223,15 +223,15 @@
   "o \<Rightarrow> o \<Rightarrow> bool"} is chosen. To choose another mode for the argument,
   you can declare the mode for the argument between the @{command
   "values"} and the number of elements.
-*}
+\<close>
 
 values %quote [mode: i \<Rightarrow> o \<Rightarrow> bool] 1 "{n. tranclp succ 10 n}" (*FIMXE does not terminate for n\<ge>1*)
 values %quote [mode: o \<Rightarrow> i \<Rightarrow> bool] 1 "{n. tranclp succ n 10}"
 
 
-subsection {* Embedding into functional code within Isabelle/HOL *}
+subsection \<open>Embedding into functional code within Isabelle/HOL\<close>
 
-text {*
+text \<open>
   To embed the computation of an inductive predicate into functions
   that are defined in Isabelle/HOL, you have a number of options:
 
@@ -258,18 +258,18 @@
       raises a run-time error @{term "not_unique"}.
 
   \end{itemize}
-*}
+\<close>
 
 
-subsection {* Further Examples *}
+subsection \<open>Further Examples\<close>
 
-text {*
+text \<open>
   Further examples for compiling inductive predicates can be found in
   @{file "~~/src/HOL/Predicate_Compile_Examples/Examples.thy"}.  There are
   also some examples in the Archive of Formal Proofs, notably in the
   @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"}
   sessions.
-*}
+\<close>
 
 end
 
diff -r ead400fd6484 -r 056945909f60 src/Doc/Codegen/Introduction.thy
--- a/src/Doc/Codegen/Introduction.thy	Thu Jan 15 13:39:41 2015 +0100
+++ b/src/Doc/Codegen/Introduction.thy	Thu Jan 15 13:39:41 2015 +0100
@@ -2,9 +2,9 @@
 imports Setup
 begin
 
-section {* Introduction *}
+section \<open>Introduction\<close>
 
-text {*
+text \<open>
   This tutorial introduces the code generator facilities of @{text
   "Isabelle/HOL"}.  It allows to turn (a certain class of) HOL
   specifications into corresponding executable code in the programming
@@ -14,12 +14,12 @@
 
   To profit from this tutorial, some familiarity and experience with
   @{theory HOL} @{cite "isa-tutorial"} and its basic theories is assumed.
-*}
+\<close>
 
 
-subsection {* Code generation principle: shallow embedding \label{sec:principle} *}
+subsection \<open>Code generation principle: shallow embedding \label{sec:principle}\<close>
 
-text {*
+text \<open>
   The key concept for understanding Isabelle's code generation is
   \emph{shallow embedding}: logical entities like constants, types and
   classes are identified with corresponding entities in the target
@@ -29,12 +29,12 @@
   system, then every rewrite step performed by the program can be
   simulated in the logic, which guarantees partial correctness
   @{cite "Haftmann-Nipkow:2010:code"}.
-*}
+\<close>
 
 
-subsection {* A quick start with the Isabelle/HOL toolbox \label{sec:queue_example} *}
+subsection \<open>A quick start with the Isabelle/HOL toolbox \label{sec:queue_example}\<close>
 
-text {*
+text \<open>
   In a HOL theory, the @{command_def datatype} and @{command_def
   definition}/@{command_def primrec}/@{command_def fun} declarations
   form the core of a functional programming language.  By default
@@ -43,7 +43,7 @@
   ado.
 
   For example, here a simple \qt{implementation} of amortised queues:
-*}
+\<close>
 
 datatype %quote 'a queue = AQueue "'a list" "'a list"
 
@@ -63,18 +63,18 @@
   "xs \<noteq> [] \<Longrightarrow> dequeue (AQueue xs []) = (case rev xs of y # ys \<Rightarrow> (Some y, AQueue [] ys))"
   by (cases xs) (simp_all split: list.splits) (*>*)
 
-text {* \noindent Then we can generate code e.g.~for @{text SML} as follows: *}
+text \<open>\noindent Then we can generate code e.g.~for @{text SML} as follows:\<close>
 
 export_code %quote empty dequeue enqueue in SML
   module_name Example file "$ISABELLE_TMP/examples/example.ML"
 
-text {* \noindent resulting in the following code: *}
+text \<open>\noindent resulting in the following code:\<close>
 
-text %quotetypewriter {*
+text %quotetypewriter \<open>
   @{code_stmts empty enqueue dequeue (SML)}
-*}
+\<close>
 
-text {*
+text \<open>
   \noindent The @{command_def export_code} command takes a
   space-separated list of constants for which code shall be generated;
   anything else needed for those is added implicitly.  Then follows a
@@ -84,31 +84,31 @@
   @{text SML}, @{text OCaml} and @{text Scala} it denotes a \emph{file},
   for @{text Haskell} it denotes a \emph{directory} where a file named as the
   module name (with extension @{text ".hs"}) is written:
-*}
+\<close>
 
 export_code %quote empty dequeue enqueue in Haskell
   module_name Example file "$ISABELLE_TMP/examples/"
 
-text {*
+text \<open>
   \noindent This is the corresponding code:
-*}
+\<close>
 
-text %quotetypewriter {*
+text %quotetypewriter \<open>
   @{code_stmts empty enqueue dequeue (Haskell)}
-*}
+\<close>
 
-text {*
+text \<open>
   \noindent For more details about @{command export_code} see
   \secref{sec:further}.
-*}
+\<close>
 
 
-subsection {* Type classes *}
+subsection \<open>Type classes\<close>
 
-text {*
+text \<open>
   Code can also be generated from type classes in a Haskell-like
   manner.  For illustration here an example from abstract algebra:
-*}
+\<close>
 
 class %quote semigroup =
   fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70)
@@ -146,51 +146,51 @@
 
 end %quote
 
-text {*
+text \<open>
   \noindent We define the natural operation of the natural numbers
   on monoids:
-*}
+\<close>
 
 primrec %quote (in monoid) pow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
     "pow 0 a = \<one>"
   | "pow (Suc n) a = a \<otimes> pow n a"
 
-text {*
+text \<open>
   \noindent This we use to define the discrete exponentiation
   function:
-*}
+\<close>
 
 definition %quote bexp :: "nat \<Rightarrow> nat" where
   "bexp n = pow n (Suc (Suc 0))"
 
-text {*
+text \<open>
   \noindent The corresponding code in Haskell uses that language's
   native classes:
-*}
+\<close>
 
-text %quotetypewriter {*
+text %quotetypewriter \<open>
   @{code_stmts bexp (Haskell)}
-*}
+\<close>
 
-text {*
+text \<open>
   \noindent This is a convenient place to show how explicit dictionary
   construction manifests in generated code -- the same example in
   @{text SML}:
-*}
+\<close>
 
-text %quotetypewriter {*
+text %quotetypewriter \<open>
   @{code_stmts bexp (SML)}
-*}
+\<close>
 
-text {*
+text \<open>
   \noindent Note the parameters with trailing underscore (@{verbatim
   "A_"}), which are the dictionary parameters.
-*}
+\<close>
 
 
-subsection {* How to continue from here *}
+subsection \<open>How to continue from here\<close>
 
-text {*
+text \<open>
   What you have seen so far should be already enough in a lot of
   cases.  If you are content with this, you can quit reading here.
 
@@ -236,7 +236,7 @@
     \begin{center}\textit{Happy proving, happy hacking!}\end{center}
 
   \end{minipage}}}\end{center}
-*}
+\<close>
 
 end
 
diff -r ead400fd6484 -r 056945909f60 src/Doc/Codegen/Refinement.thy
--- a/src/Doc/Codegen/Refinement.thy	Thu Jan 15 13:39:41 2015 +0100
+++ b/src/Doc/Codegen/Refinement.thy	Thu Jan 15 13:39:41 2015 +0100
@@ -2,81 +2,81 @@
 imports Setup
 begin
 
-section {* Program and datatype refinement \label{sec:refinement} *}
+section \<open>Program and datatype refinement \label{sec:refinement}\<close>
 
-text {*
+text \<open>
   Code generation by shallow embedding (cf.~\secref{sec:principle})
   allows to choose code equations and datatype constructors freely,
   given that some very basic syntactic properties are met; this
   flexibility opens up mechanisms for refinement which allow to extend
   the scope and quality of generated code dramatically.
-*}
+\<close>
 
 
-subsection {* Program refinement *}
+subsection \<open>Program refinement\<close>
 
-text {*
+text \<open>
   Program refinement works by choosing appropriate code equations
   explicitly (cf.~\secref{sec:equations}); as example, we use Fibonacci
   numbers:
-*}
+\<close>
 
 fun %quote fib :: "nat \<Rightarrow> nat" where
     "fib 0 = 0"
   | "fib (Suc 0) = Suc 0"
   | "fib (Suc (Suc n)) = fib n + fib (Suc n)"
 
-text {*
+text \<open>
   \noindent The runtime of the corresponding code grows exponential due
   to two recursive calls:
-*}
+\<close>
 
-text %quotetypewriter {*
+text %quotetypewriter \<open>
   @{code_stmts fib (consts) fib (Haskell)}
-*}
+\<close>
 
-text {*
+text \<open>
   \noindent A more efficient implementation would use dynamic
   programming, e.g.~sharing of common intermediate results between
   recursive calls.  This idea is expressed by an auxiliary operation
   which computes a Fibonacci number and its successor simultaneously:
-*}
+\<close>
 
 definition %quote fib_step :: "nat \<Rightarrow> nat \<times> nat" where
   "fib_step n = (fib (Suc n), fib n)"
 
-text {*
+text \<open>
   \noindent This operation can be implemented by recursion using
   dynamic programming:
-*}
+\<close>
 
 lemma %quote [code]:
   "fib_step 0 = (Suc 0, 0)"
   "fib_step (Suc n) = (let (m, q) = fib_step n in (m + q, m))"
   by (simp_all add: fib_step_def)
 
-text {*
+text \<open>
   \noindent What remains is to implement @{const fib} by @{const
   fib_step} as follows:
-*}
+\<close>
 
 lemma %quote [code]:
   "fib 0 = 0"
   "fib (Suc n) = fst (fib_step n)"
   by (simp_all add: fib_step_def)
 
-text {*
+text \<open>
   \noindent The resulting code shows only linear growth of runtime:
-*}
+\<close>
 
-text %quotetypewriter {*
+text %quotetypewriter \<open>
   @{code_stmts fib (consts) fib fib_step (Haskell)}
-*}
+\<close>
 
 
-subsection {* Datatype refinement *}
+subsection \<open>Datatype refinement\<close>
 
-text {*
+text \<open>
   Selecting specific code equations \emph{and} datatype constructors
   leads to datatype refinement.  As an example, we will develop an
   alternative representation of the queue example given in
@@ -85,7 +85,7 @@
   details, which may be cumbersome when proving theorems about it.
   Therefore, here is a simple, straightforward representation of
   queues:
-*}
+\<close>
 
 datatype %quote 'a queue = Queue "'a list"
 
@@ -99,17 +99,17 @@
     "dequeue (Queue []) = (None, Queue [])"
   | "dequeue (Queue (x # xs)) = (Some x, Queue xs)"
 
-text {*
+text \<open>
   \noindent This we can use directly for proving;  for executing,
   we provide an alternative characterisation:
-*}
+\<close>
 
 definition %quote AQueue :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a queue" where
   "AQueue xs ys = Queue (ys @ rev xs)"
 
 code_datatype %quote AQueue
 
-text {*
+text \<open>
   \noindent Here we define a \qt{constructor} @{const "AQueue"} which
   is defined in terms of @{text "Queue"} and interprets its arguments
   according to what the \emph{content} of an amortised queue is supposed
@@ -127,7 +127,7 @@
   Equipped with this, we are able to prove the following equations
   for our primitive queue operations which \qt{implement} the simple
   queues in an amortised fashion:
-*}
+\<close>
 
 lemma %quote empty_AQueue [code]:
   "empty = AQueue [] []"
@@ -144,12 +144,12 @@
   "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
   by (simp_all add: AQueue_def)
 
-text {*
+text \<open>
   \noindent It is good style, although no absolute requirement, to
   provide code equations for the original artefacts of the implemented
   type, if possible; in our case, these are the datatype constructor
   @{const Queue} and the case combinator @{const case_queue}:
-*}
+\<close>
 
 lemma %quote Queue_AQueue [code]:
   "Queue = AQueue []"
@@ -159,15 +159,15 @@
   "case_queue f (AQueue xs ys) = f (ys @ rev xs)"
   by (simp add: AQueue_def)
 
-text {*
+text \<open>
   \noindent The resulting code looks as expected:
-*}
+\<close>
 
-text %quotetypewriter {*
+text %quotetypewriter \<open>
   @{code_stmts empty enqueue dequeue Queue case_queue (SML)}
-*}
+\<close>
 
-text {*
+text \<open>
   The same techniques can also be applied to types which are not
   specified as datatypes, e.g.~type @{typ int} is originally specified
   as quotient type by means of @{command_def typedef}, but for code
@@ -176,12 +176,12 @@
 
   This approach however fails if the representation of a type demands
   invariants; this issue is discussed in the next section.
-*}
+\<close>
 
 
-subsection {* Datatype refinement involving invariants \label{sec:invariant} *}
+subsection \<open>Datatype refinement involving invariants \label{sec:invariant}\<close>
 
-text {*
+text \<open>
   Datatype representation involving invariants require a dedicated
   setup for the type and its primitive operations.  As a running
   example, we implement a type @{text "'a dlist"} of list consisting
@@ -191,31 +191,31 @@
   type (in our example @{text "'a dlist"}) should be implemented.
   Here we choose @{text "'a list"}.  Then a conversion from the concrete
   type to the abstract type must be specified, here:
-*}
+\<close>
 
-text %quote {*
+text %quote \<open>
   @{term_type Dlist}
-*}
+\<close>
 
-text {*
+text \<open>
   \noindent Next follows the specification of a suitable \emph{projection},
   i.e.~a conversion from abstract to concrete type:
-*}
+\<close>
 
-text %quote {*
+text %quote \<open>
   @{term_type list_of_dlist}
-*}
+\<close>
 
-text {*
+text \<open>
   \noindent This projection must be specified such that the following
   \emph{abstract datatype certificate} can be proven:
-*}
+\<close>
 
 lemma %quote [code abstype]:
   "Dlist (list_of_dlist dxs) = dxs"
   by (fact Dlist_list_of_dlist)
 
-text {*
+text \<open>
   \noindent Note that so far the invariant on representations
   (@{term_type distinct}) has never been mentioned explicitly:
   the invariant is only referred to implicitly: all values in
@@ -226,26 +226,26 @@
   indirectly using the projection @{const list_of_dlist}.  For
   the empty @{text "dlist"}, @{const Dlist.empty}, we finally want
   the code equation
-*}
+\<close>
 
-text %quote {*
+text %quote \<open>
   @{term "Dlist.empty = Dlist []"}
-*}
+\<close>
 
-text {*
+text \<open>
   \noindent This we have to prove indirectly as follows:
-*}
+\<close>
 
 lemma %quote [code]:
   "list_of_dlist Dlist.empty = []"
   by (fact list_of_dlist_empty)
 
-text {*
+text \<open>
   \noindent This equation logically encodes both the desired code
   equation and that the expression @{const Dlist} is applied to obeys
   the implicit invariant.  Equations for insertion and removal are
   similar:
-*}
+\<close>
 
 lemma %quote [code]:
   "list_of_dlist (Dlist.insert x dxs) = List.insert x (list_of_dlist dxs)"
@@ -255,15 +255,15 @@
   "list_of_dlist (Dlist.remove x dxs) = remove1 x (list_of_dlist dxs)"
   by (fact list_of_dlist_remove)
 
-text {*
+text \<open>
   \noindent Then the corresponding code is as follows:
-*}
+\<close>
 
-text %quotetypewriter {*
+text %quotetypewriter \<open>
   @{code_stmts Dlist.empty Dlist.insert Dlist.remove list_of_dlist (Haskell)}
-*}
+\<close>
 
-text {*
+text \<open>
   See further @{cite "Haftmann-Kraus-Kuncar-Nipkow:2013:data_refinement"}
   for the meta theory of datatype refinement involving invariants.
 
@@ -271,6 +271,6 @@
   invariants are available in the library, theory @{theory Mapping}
   specifies key-value-mappings (type @{typ "('a, 'b) mapping"});
   these can be implemented by red-black-trees (theory @{theory RBT}).
-*}
+\<close>
 
 end
diff -r ead400fd6484 -r 056945909f60 src/Doc/Codegen/Setup.thy
--- a/src/Doc/Codegen/Setup.thy	Thu Jan 15 13:39:41 2015 +0100
+++ b/src/Doc/Codegen/Setup.thy	Thu Jan 15 13:39:41 2015 +0100
@@ -14,7 +14,7 @@
 ML_file "../antiquote_setup.ML"
 ML_file "../more_antiquote.ML"
 
-setup {*
+setup \<open>
 let
   val typ = Simple_Syntax.read_typ;
 in
@@ -25,7 +25,7 @@
    [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
     ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
 end
-*}
+\<close>
 
 declare [[default_code_width = 74]]