# HG changeset patch
# User haftmann
# Date 1282911929 -7200
# Node ID d0196406ee325d0276d037c9a334d59c6b25245e
# Parent  abe92b33ac9f656d2b289f1489f2e42aa1438a37# Parent  4d575fbfc920e3aa649eb1d82a537235d6ca2d32
merged

diff -r abe92b33ac9f -r d0196406ee32 NEWS
--- a/NEWS	Fri Aug 27 12:57:55 2010 +0200
+++ b/NEWS	Fri Aug 27 14:25:29 2010 +0200
@@ -56,6 +56,9 @@
 
 *** HOL ***
 
+* Scala (2.8 or higher) has been added to the target languages of
+the code generator.
+
 * Dropped type classes mult_mono and mult_mono1.  INCOMPATIBILITY.
 
 * Theory SetsAndFunctions has been split into Function_Algebras and Set_Algebras;
diff -r abe92b33ac9f -r d0196406ee32 doc-src/Classes/Thy/Classes.thy
--- a/doc-src/Classes/Thy/Classes.thy	Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/Classes/Thy/Classes.thy	Fri Aug 27 14:25:29 2010 +0200
@@ -8,14 +8,14 @@
   Type classes were introduced by Wadler and Blott \cite{wadler89how}
   into the Haskell language to allow for a reasonable implementation
   of overloading\footnote{throughout this tutorial, we are referring
-  to classical Haskell 1.0 type classes, not considering
-  later additions in expressiveness}.
-  As a canonical example, a polymorphic equality function
-  @{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} which is overloaded on different
-  types for @{text "\<alpha>"}, which is achieved by splitting introduction
-  of the @{text eq} function from its overloaded definitions by means
-  of @{text class} and @{text instance} declarations:
-  \footnote{syntax here is a kind of isabellized Haskell}
+  to classical Haskell 1.0 type classes, not considering later
+  additions in expressiveness}.  As a canonical example, a polymorphic
+  equality function @{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} which is overloaded on
+  different types for @{text "\<alpha>"}, which is achieved by splitting
+  introduction of the @{text eq} function from its overloaded
+  definitions by means of @{text class} and @{text instance}
+  declarations: \footnote{syntax here is a kind of isabellized
+  Haskell}
 
   \begin{quote}
 
@@ -41,14 +41,14 @@
   these annotations are assertions that a particular polymorphic type
   provides definitions for overloaded functions.
 
-  Indeed, type classes not only allow for simple overloading
-  but form a generic calculus, an instance of order-sorted
-  algebra \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
+  Indeed, type classes not only allow for simple overloading but form
+  a generic calculus, an instance of order-sorted algebra
+  \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
 
-  From a software engineering point of view, type classes
-  roughly correspond to interfaces in object-oriented languages like Java;
-  so, it is naturally desirable that type classes do not only
-  provide functions (class parameters) but also state specifications
+  From a software engineering point of view, type classes roughly
+  correspond to interfaces in object-oriented languages like Java; so,
+  it is naturally desirable that type classes do not only provide
+  functions (class parameters) but also state specifications
   implementations must obey.  For example, the @{text "class eq"}
   above could be given the following specification, demanding that
   @{text "class eq"} is an equivalence relation obeying reflexivity,
@@ -65,11 +65,10 @@
 
   \end{quote}
 
-  \noindent From a theoretical point of view, type classes are lightweight
-  modules; Haskell type classes may be emulated by
-  SML functors \cite{classes_modules}. 
-  Isabelle/Isar offers a discipline of type classes which brings
-  all those aspects together:
+  \noindent From a theoretical point of view, type classes are
+  lightweight modules; Haskell type classes may be emulated by SML
+  functors \cite{classes_modules}.  Isabelle/Isar offers a discipline
+  of type classes which brings all those aspects together:
 
   \begin{enumerate}
     \item specifying abstract parameters together with
@@ -81,15 +80,15 @@
       locales \cite{kammueller-locales}.
   \end{enumerate}
 
-  \noindent Isar type classes also directly support code generation
-  in a Haskell like fashion. Internally, they are mapped to more primitive 
-  Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
+  \noindent Isar type classes also directly support code generation in
+  a Haskell like fashion. Internally, they are mapped to more
+  primitive Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
 
-  This tutorial demonstrates common elements of structured specifications
-  and abstract reasoning with type classes by the algebraic hierarchy of
-  semigroups, monoids and groups.  Our background theory is that of
-  Isabelle/HOL \cite{isa-tutorial}, for which some
-  familiarity is assumed.
+  This tutorial demonstrates common elements of structured
+  specifications and abstract reasoning with type classes by the
+  algebraic hierarchy of semigroups, monoids and groups.  Our
+  background theory is that of Isabelle/HOL \cite{isa-tutorial}, for
+  which some familiarity is assumed.
 *}
 
 section {* A simple algebra example \label{sec:example} *}
@@ -107,25 +106,24 @@
   assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
 
 text {*
-  \noindent This @{command class} specification consists of two
-  parts: the \qn{operational} part names the class parameter
-  (@{element "fixes"}), the \qn{logical} part specifies properties on them
-  (@{element "assumes"}).  The local @{element "fixes"} and
-  @{element "assumes"} are lifted to the theory toplevel,
-  yielding the global
+  \noindent This @{command class} specification consists of two parts:
+  the \qn{operational} part names the class parameter (@{element
+  "fixes"}), the \qn{logical} part specifies properties on them
+  (@{element "assumes"}).  The local @{element "fixes"} and @{element
+  "assumes"} are lifted to the theory toplevel, yielding the global
   parameter @{term [source] "mult \<Colon> \<alpha>\<Colon>semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the
-  global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\<And>x y
-  z \<Colon> \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
+  global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\<And>x y z \<Colon>
+  \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
 *}
 
 
 subsection {* Class instantiation \label{sec:class_inst} *}
 
 text {*
-  The concrete type @{typ int} is made a @{class semigroup}
-  instance by providing a suitable definition for the class parameter
-  @{text "(\<otimes>)"} and a proof for the specification of @{fact assoc}.
-  This is accomplished by the @{command instantiation} target:
+  The concrete type @{typ int} is made a @{class semigroup} instance
+  by providing a suitable definition for the class parameter @{text
+  "(\<otimes>)"} and a proof for the specification of @{fact assoc}.  This is
+  accomplished by the @{command instantiation} target:
 *}
 
 instantiation %quote int :: semigroup
@@ -143,22 +141,22 @@
 end %quote
 
 text {*
-  \noindent @{command instantiation} defines class parameters
-  at a particular instance using common specification tools (here,
-  @{command definition}).  The concluding @{command instance}
-  opens a proof that the given parameters actually conform
-  to the class specification.  Note that the first proof step
-  is the @{method default} method,
-  which for such instance proofs maps to the @{method intro_classes} method.
-  This reduces an instance judgement to the relevant primitive
-  proof goals; typically it is the first method applied
-  in an instantiation proof.
+  \noindent @{command instantiation} defines class parameters at a
+  particular instance using common specification tools (here,
+  @{command definition}).  The concluding @{command instance} opens a
+  proof that the given parameters actually conform to the class
+  specification.  Note that the first proof step is the @{method
+  default} method, which for such instance proofs maps to the @{method
+  intro_classes} method.  This reduces an instance judgement to the
+  relevant primitive proof goals; typically it is the first method
+  applied in an instantiation proof.
 
-  From now on, the type-checker will consider @{typ int}
-  as a @{class semigroup} automatically, i.e.\ any general results
-  are immediately available on concrete instances.
+  From now on, the type-checker will consider @{typ int} as a @{class
+  semigroup} automatically, i.e.\ any general results are immediately
+  available on concrete instances.
 
-  \medskip Another instance of @{class semigroup} yields the natural numbers:
+  \medskip Another instance of @{class semigroup} yields the natural
+  numbers:
 *}
 
 instantiation %quote nat :: semigroup
@@ -177,21 +175,20 @@
 end %quote
 
 text {*
-  \noindent Note the occurence of the name @{text mult_nat}
-  in the primrec declaration;  by default, the local name of
-  a class operation @{text f} to be instantiated on type constructor
-  @{text \<kappa>} is mangled as @{text f_\<kappa>}.  In case of uncertainty,
-  these names may be inspected using the @{command "print_context"} command
-  or the corresponding ProofGeneral button.
+  \noindent Note the occurence of the name @{text mult_nat} in the
+  primrec declaration; by default, the local name of a class operation
+  @{text f} to be instantiated on type constructor @{text \<kappa>} is
+  mangled as @{text f_\<kappa>}.  In case of uncertainty, these names may be
+  inspected using the @{command "print_context"} command or the
+  corresponding ProofGeneral button.
 *}
 
 subsection {* Lifting and parametric types *}
 
 text {*
-  Overloaded definitions given at a class instantiation
-  may include recursion over the syntactic structure of types.
-  As a canonical example, we model product semigroups
-  using our simple algebra:
+  Overloaded definitions given at a class instantiation may include
+  recursion over the syntactic structure of types.  As a canonical
+  example, we model product semigroups using our simple algebra:
 *}
 
 instantiation %quote prod :: (semigroup, semigroup) semigroup
@@ -211,21 +208,19 @@
 text {*
   \noindent Associativity of product semigroups is established using
   the definition of @{text "(\<otimes>)"} on products and the hypothetical
-  associativity of the type components;  these hypotheses
-  are legitimate due to the @{class semigroup} constraints imposed
-  on the type components by the @{command instance} proposition.
-  Indeed, this pattern often occurs with parametric types
-  and type classes.
+  associativity of the type components; these hypotheses are
+  legitimate due to the @{class semigroup} constraints imposed on the
+  type components by the @{command instance} proposition.  Indeed,
+  this pattern often occurs with parametric types and type classes.
 *}
 
 
 subsection {* Subclassing *}
 
 text {*
-  We define a subclass @{text monoidl} (a semigroup with a left-hand neutral)
-  by extending @{class semigroup}
-  with one additional parameter @{text neutral} together
-  with its characteristic property:
+  We define a subclass @{text monoidl} (a semigroup with a left-hand
+  neutral) by extending @{class semigroup} with one additional
+  parameter @{text neutral} together with its characteristic property:
 *}
 
 class %quote monoidl = semigroup +
@@ -233,10 +228,10 @@
   assumes neutl: "\<one> \<otimes> x = x"
 
 text {*
-  \noindent Again, we prove some instances, by
-  providing suitable parameter definitions and proofs for the
-  additional specifications.  Observe that instantiations
-  for types with the same arity may be simultaneous:
+  \noindent Again, we prove some instances, by providing suitable
+  parameter definitions and proofs for the additional specifications.
+  Observe that instantiations for types with the same arity may be
+  simultaneous:
 *}
 
 instantiation %quote nat and int :: monoidl
@@ -309,8 +304,8 @@
 end %quote
 
 text {*
-  \noindent To finish our small algebra example, we add a @{text group} class
-  with a corresponding instance:
+  \noindent To finish our small algebra example, we add a @{text
+  group} class with a corresponding instance:
 *}
 
 class %quote group = monoidl +
@@ -338,9 +333,9 @@
 subsection {* A look behind the scenes *}
 
 text {*
-  The example above gives an impression how Isar type classes work
-  in practice.  As stated in the introduction, classes also provide
-  a link to Isar's locale system.  Indeed, the logical core of a class
+  The example above gives an impression how Isar type classes work in
+  practice.  As stated in the introduction, classes also provide a
+  link to Isar's locale system.  Indeed, the logical core of a class
   is nothing other than a locale:
 *}
 
@@ -402,13 +397,14 @@
 qed
 
 text {*
-  \noindent Here the \qt{@{keyword "in"} @{class group}} target specification
-  indicates that the result is recorded within that context for later
-  use.  This local theorem is also lifted to the global one @{fact
-  "group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon> \<alpha>\<Colon>group. x \<otimes> y = x \<otimes>
-  z \<longleftrightarrow> y = z"}.  Since type @{text "int"} has been made an instance of
-  @{text "group"} before, we may refer to that fact as well: @{prop
-  [source] "\<And>x y z \<Colon> int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}.
+  \noindent Here the \qt{@{keyword "in"} @{class group}} target
+  specification indicates that the result is recorded within that
+  context for later use.  This local theorem is also lifted to the
+  global one @{fact "group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon>
+  \<alpha>\<Colon>group. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}.  Since type @{text "int"} has been
+  made an instance of @{text "group"} before, we may refer to that
+  fact as well: @{prop [source] "\<And>x y z \<Colon> int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y =
+  z"}.
 *}
 
 
@@ -424,15 +420,14 @@
 
 text {*
   \noindent If the locale @{text group} is also a class, this local
-  definition is propagated onto a global definition of
-  @{term [source] "pow_nat \<Colon> nat \<Rightarrow> \<alpha>\<Colon>monoid \<Rightarrow> \<alpha>\<Colon>monoid"}
-  with corresponding theorems
+  definition is propagated onto a global definition of @{term [source]
+  "pow_nat \<Colon> nat \<Rightarrow> \<alpha>\<Colon>monoid \<Rightarrow> \<alpha>\<Colon>monoid"} with corresponding theorems
 
   @{thm pow_nat.simps [no_vars]}.
 
-  \noindent As you can see from this example, for local
-  definitions you may use any specification tool
-  which works together with locales, such as Krauss's recursive function package
+  \noindent As you can see from this example, for local definitions
+  you may use any specification tool which works together with
+  locales, such as Krauss's recursive function package
   \cite{krauss2006}.
 *}
 
@@ -440,19 +435,17 @@
 subsection {* A functor analogy *}
 
 text {*
-  We introduced Isar classes by analogy to type classes in
-  functional programming;  if we reconsider this in the
-  context of what has been said about type classes and locales,
-  we can drive this analogy further by stating that type
-  classes essentially correspond to functors that have
-  a canonical interpretation as type classes.
-  There is also the possibility of other interpretations.
-  For example, @{text list}s also form a monoid with
-  @{text append} and @{term "[]"} as operations, but it
-  seems inappropriate to apply to lists
-  the same operations as for genuinely algebraic types.
-  In such a case, we can simply make a particular interpretation
-  of monoids for lists:
+  We introduced Isar classes by analogy to type classes in functional
+  programming; if we reconsider this in the context of what has been
+  said about type classes and locales, we can drive this analogy
+  further by stating that type classes essentially correspond to
+  functors that have a canonical interpretation as type classes.
+  There is also the possibility of other interpretations.  For
+  example, @{text list}s also form a monoid with @{text append} and
+  @{term "[]"} as operations, but it seems inappropriate to apply to
+  lists the same operations as for genuinely algebraic types.  In such
+  a case, we can simply make a particular interpretation of monoids
+  for lists:
 *}
 
 interpretation %quote list_monoid: monoid append "[]"
@@ -510,12 +503,10 @@
 qed
 
 text {*
-  The logical proof is carried out on the locale level.
-  Afterwards it is propagated
-  to the type system, making @{text group} an instance of
-  @{text monoid} by adding an additional edge
-  to the graph of subclass relations
-  (\figref{fig:subclass}).
+  The logical proof is carried out on the locale level.  Afterwards it
+  is propagated to the type system, making @{text group} an instance
+  of @{text monoid} by adding an additional edge to the graph of
+  subclass relations (\figref{fig:subclass}).
 
   \begin{figure}[htbp]
    \begin{center}
@@ -547,8 +538,8 @@
    \end{center}
   \end{figure}
 
-  For illustration, a derived definition
-  in @{text group} using @{text pow_nat}
+  For illustration, a derived definition in @{text group} using @{text
+  pow_nat}
 *}
 
 definition %quote (in group) pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
@@ -557,17 +548,17 @@
     else (pow_nat (nat (- k)) x)\<div>)"
 
 text {*
-  \noindent yields the global definition of
-  @{term [source] "pow_int \<Colon> int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"}
-  with the corresponding theorem @{thm pow_int_def [no_vars]}.
+  \noindent yields the global definition of @{term [source] "pow_int \<Colon>
+  int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"} with the corresponding theorem @{thm
+  pow_int_def [no_vars]}.
 *}
 
 subsection {* A note on syntax *}
 
 text {*
-  As a convenience, class context syntax allows references
-  to local class operations and their global counterparts
-  uniformly;  type inference resolves ambiguities.  For example:
+  As a convenience, class context syntax allows references to local
+  class operations and their global counterparts uniformly; type
+  inference resolves ambiguities.  For example:
 *}
 
 context %quote semigroup
@@ -581,11 +572,11 @@
 term %quote "x \<otimes> y" -- {* example 3 *}
 
 text {*
-  \noindent Here in example 1, the term refers to the local class operation
-  @{text "mult [\<alpha>]"}, whereas in example 2 the type constraint
-  enforces the global class operation @{text "mult [nat]"}.
-  In the global context in example 3, the reference is
-  to the polymorphic global class operation @{text "mult [?\<alpha> \<Colon> semigroup]"}.
+  \noindent Here in example 1, the term refers to the local class
+  operation @{text "mult [\<alpha>]"}, whereas in example 2 the type
+  constraint enforces the global class operation @{text "mult [nat]"}.
+  In the global context in example 3, the reference is to the
+  polymorphic global class operation @{text "mult [?\<alpha> \<Colon> semigroup]"}.
 *}
 
 section {* Further issues *}
@@ -593,16 +584,14 @@
 subsection {* Type classes and code generation *}
 
 text {*
-  Turning back to the first motivation for type classes,
-  namely overloading, it is obvious that overloading
-  stemming from @{command class} statements and
-  @{command instantiation}
-  targets naturally maps to Haskell type classes.
-  The code generator framework \cite{isabelle-codegen} 
-  takes this into account.  If the target language (e.g.~SML)
-  lacks type classes, then they
-  are implemented by an explicit dictionary construction.
-  As example, let's go back to the power function:
+  Turning back to the first motivation for type classes, namely
+  overloading, it is obvious that overloading stemming from @{command
+  class} statements and @{command instantiation} targets naturally
+  maps to Haskell type classes.  The code generator framework
+  \cite{isabelle-codegen} takes this into account.  If the target
+  language (e.g.~SML) lacks type classes, then they are implemented by
+  an explicit dictionary construction.  As example, let's go back to
+  the power function:
 *}
 
 definition %quote example :: int where
@@ -619,11 +608,18 @@
 *}
 text %quote {*@{code_stmts example (SML)}*}
 
+text {*
+  \noindent In Scala, implicts are used as dictionaries:
+*}
+(*<*)code_include %invisible Scala "Natural" -(*>*)
+text %quote {*@{code_stmts example (Scala)}*}
+
+
 subsection {* Inspecting the type class universe *}
 
 text {*
-  To facilitate orientation in complex subclass structures,
-  two diagnostics commands are provided:
+  To facilitate orientation in complex subclass structures, two
+  diagnostics commands are provided:
 
   \begin{description}
 
diff -r abe92b33ac9f -r d0196406ee32 doc-src/Classes/Thy/document/Classes.tex
--- a/doc-src/Classes/Thy/document/Classes.tex	Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex	Fri Aug 27 14:25:29 2010 +0200
@@ -26,14 +26,14 @@
 Type classes were introduced by Wadler and Blott \cite{wadler89how}
   into the Haskell language to allow for a reasonable implementation
   of overloading\footnote{throughout this tutorial, we are referring
-  to classical Haskell 1.0 type classes, not considering
-  later additions in expressiveness}.
-  As a canonical example, a polymorphic equality function
-  \isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} which is overloaded on different
-  types for \isa{{\isasymalpha}}, which is achieved by splitting introduction
-  of the \isa{eq} function from its overloaded definitions by means
-  of \isa{class} and \isa{instance} declarations:
-  \footnote{syntax here is a kind of isabellized Haskell}
+  to classical Haskell 1.0 type classes, not considering later
+  additions in expressiveness}.  As a canonical example, a polymorphic
+  equality function \isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} which is overloaded on
+  different types for \isa{{\isasymalpha}}, which is achieved by splitting
+  introduction of the \isa{eq} function from its overloaded
+  definitions by means of \isa{class} and \isa{instance}
+  declarations: \footnote{syntax here is a kind of isabellized
+  Haskell}
 
   \begin{quote}
 
@@ -59,14 +59,14 @@
   these annotations are assertions that a particular polymorphic type
   provides definitions for overloaded functions.
 
-  Indeed, type classes not only allow for simple overloading
-  but form a generic calculus, an instance of order-sorted
-  algebra \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
+  Indeed, type classes not only allow for simple overloading but form
+  a generic calculus, an instance of order-sorted algebra
+  \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
 
-  From a software engineering point of view, type classes
-  roughly correspond to interfaces in object-oriented languages like Java;
-  so, it is naturally desirable that type classes do not only
-  provide functions (class parameters) but also state specifications
+  From a software engineering point of view, type classes roughly
+  correspond to interfaces in object-oriented languages like Java; so,
+  it is naturally desirable that type classes do not only provide
+  functions (class parameters) but also state specifications
   implementations must obey.  For example, the \isa{class\ eq}
   above could be given the following specification, demanding that
   \isa{class\ eq} is an equivalence relation obeying reflexivity,
@@ -83,11 +83,10 @@
 
   \end{quote}
 
-  \noindent From a theoretical point of view, type classes are lightweight
-  modules; Haskell type classes may be emulated by
-  SML functors \cite{classes_modules}. 
-  Isabelle/Isar offers a discipline of type classes which brings
-  all those aspects together:
+  \noindent From a theoretical point of view, type classes are
+  lightweight modules; Haskell type classes may be emulated by SML
+  functors \cite{classes_modules}.  Isabelle/Isar offers a discipline
+  of type classes which brings all those aspects together:
 
   \begin{enumerate}
     \item specifying abstract parameters together with
@@ -99,15 +98,15 @@
       locales \cite{kammueller-locales}.
   \end{enumerate}
 
-  \noindent Isar type classes also directly support code generation
-  in a Haskell like fashion. Internally, they are mapped to more primitive 
-  Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
+  \noindent Isar type classes also directly support code generation in
+  a Haskell like fashion. Internally, they are mapped to more
+  primitive Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
 
-  This tutorial demonstrates common elements of structured specifications
-  and abstract reasoning with type classes by the algebraic hierarchy of
-  semigroups, monoids and groups.  Our background theory is that of
-  Isabelle/HOL \cite{isa-tutorial}, for which some
-  familiarity is assumed.%
+  This tutorial demonstrates common elements of structured
+  specifications and abstract reasoning with type classes by the
+  algebraic hierarchy of semigroups, monoids and groups.  Our
+  background theory is that of Isabelle/HOL \cite{isa-tutorial}, for
+  which some familiarity is assumed.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -142,12 +141,9 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent This \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} specification consists of two
-  parts: the \qn{operational} part names the class parameter
-  (\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}), the \qn{logical} part specifies properties on them
-  (\hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}).  The local \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} and
-  \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} are lifted to the theory toplevel,
-  yielding the global
+\noindent This \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} specification consists of two parts:
+  the \qn{operational} part names the class parameter (\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}), the \qn{logical} part specifies properties on them
+  (\hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}).  The local \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} and \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} are lifted to the theory toplevel, yielding the global
   parameter \isa{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the
   global theorem \hyperlink{fact.semigroup.assoc:}{\mbox{\isa{semigroup{\isachardot}assoc{\isacharcolon}}}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.%
 \end{isamarkuptext}%
@@ -158,10 +154,9 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-The concrete type \isa{int} is made a \isa{semigroup}
-  instance by providing a suitable definition for the class parameter
-  \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} and a proof for the specification of \hyperlink{fact.assoc}{\mbox{\isa{assoc}}}.
-  This is accomplished by the \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} target:%
+The concrete type \isa{int} is made a \isa{semigroup} instance
+  by providing a suitable definition for the class parameter \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} and a proof for the specification of \hyperlink{fact.assoc}{\mbox{\isa{assoc}}}.  This is
+  accomplished by the \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} target:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -204,22 +199,19 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} defines class parameters
-  at a particular instance using common specification tools (here,
-  \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}).  The concluding \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}
-  opens a proof that the given parameters actually conform
-  to the class specification.  Note that the first proof step
-  is the \hyperlink{method.default}{\mbox{\isa{default}}} method,
-  which for such instance proofs maps to the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method.
-  This reduces an instance judgement to the relevant primitive
-  proof goals; typically it is the first method applied
-  in an instantiation proof.
+\noindent \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} defines class parameters at a
+  particular instance using common specification tools (here,
+  \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}).  The concluding \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} opens a
+  proof that the given parameters actually conform to the class
+  specification.  Note that the first proof step is the \hyperlink{method.default}{\mbox{\isa{default}}} method, which for such instance proofs maps to the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method.  This reduces an instance judgement to the
+  relevant primitive proof goals; typically it is the first method
+  applied in an instantiation proof.
 
-  From now on, the type-checker will consider \isa{int}
-  as a \isa{semigroup} automatically, i.e.\ any general results
-  are immediately available on concrete instances.
+  From now on, the type-checker will consider \isa{int} as a \isa{semigroup} automatically, i.e.\ any general results are immediately
+  available on concrete instances.
 
-  \medskip Another instance of \isa{semigroup} yields the natural numbers:%
+  \medskip Another instance of \isa{semigroup} yields the natural
+  numbers:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -259,12 +251,12 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent Note the occurence of the name \isa{mult{\isacharunderscore}nat}
-  in the primrec declaration;  by default, the local name of
-  a class operation \isa{f} to be instantiated on type constructor
-  \isa{{\isasymkappa}} is mangled as \isa{f{\isacharunderscore}{\isasymkappa}}.  In case of uncertainty,
-  these names may be inspected using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isacharunderscore}context}}}} command
-  or the corresponding ProofGeneral button.%
+\noindent Note the occurence of the name \isa{mult{\isacharunderscore}nat} in the
+  primrec declaration; by default, the local name of a class operation
+  \isa{f} to be instantiated on type constructor \isa{{\isasymkappa}} is
+  mangled as \isa{f{\isacharunderscore}{\isasymkappa}}.  In case of uncertainty, these names may be
+  inspected using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isacharunderscore}context}}}} command or the
+  corresponding ProofGeneral button.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -273,10 +265,9 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Overloaded definitions given at a class instantiation
-  may include recursion over the syntactic structure of types.
-  As a canonical example, we model product semigroups
-  using our simple algebra:%
+Overloaded definitions given at a class instantiation may include
+  recursion over the syntactic structure of types.  As a canonical
+  example, we model product semigroups using our simple algebra:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -318,11 +309,10 @@
 \begin{isamarkuptext}%
 \noindent Associativity of product semigroups is established using
   the definition of \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} on products and the hypothetical
-  associativity of the type components;  these hypotheses
-  are legitimate due to the \isa{semigroup} constraints imposed
-  on the type components by the \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} proposition.
-  Indeed, this pattern often occurs with parametric types
-  and type classes.%
+  associativity of the type components; these hypotheses are
+  legitimate due to the \isa{semigroup} constraints imposed on the
+  type components by the \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} proposition.  Indeed,
+  this pattern often occurs with parametric types and type classes.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -331,10 +321,9 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-We define a subclass \isa{monoidl} (a semigroup with a left-hand neutral)
-  by extending \isa{semigroup}
-  with one additional parameter \isa{neutral} together
-  with its characteristic property:%
+We define a subclass \isa{monoidl} (a semigroup with a left-hand
+  neutral) by extending \isa{semigroup} with one additional
+  parameter \isa{neutral} together with its characteristic property:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -355,10 +344,10 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent Again, we prove some instances, by
-  providing suitable parameter definitions and proofs for the
-  additional specifications.  Observe that instantiations
-  for types with the same arity may be simultaneous:%
+\noindent Again, we prove some instances, by providing suitable
+  parameter definitions and proofs for the additional specifications.
+  Observe that instantiations for types with the same arity may be
+  simultaneous:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -505,8 +494,7 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent To finish our small algebra example, we add a \isa{group} class
-  with a corresponding instance:%
+\noindent To finish our small algebra example, we add a \isa{group} class with a corresponding instance:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -563,9 +551,9 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-The example above gives an impression how Isar type classes work
-  in practice.  As stated in the introduction, classes also provide
-  a link to Isar's locale system.  Indeed, the logical core of a class
+The example above gives an impression how Isar type classes work in
+  practice.  As stated in the introduction, classes also provide a
+  link to Isar's locale system.  Indeed, the logical core of a class
   is nothing other than a locale:%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -780,10 +768,12 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent Here the \qt{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}} \isa{group}} target specification
-  indicates that the result is recorded within that context for later
-  use.  This local theorem is also lifted to the global one \hyperlink{fact.group.left-cancel:}{\mbox{\isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}}}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.  Since type \isa{int} has been made an instance of
-  \isa{group} before, we may refer to that fact as well: \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ int{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.%
+\noindent Here the \qt{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}} \isa{group}} target
+  specification indicates that the result is recorded within that
+  context for later use.  This local theorem is also lifted to the
+  global one \hyperlink{fact.group.left-cancel:}{\mbox{\isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}}}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.  Since type \isa{int} has been
+  made an instance of \isa{group} before, we may refer to that
+  fact as well: \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ int{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -814,16 +804,14 @@
 %
 \begin{isamarkuptext}%
 \noindent If the locale \isa{group} is also a class, this local
-  definition is propagated onto a global definition of
-  \isa{{\isachardoublequote}pow{\isacharunderscore}nat\ {\isasymColon}\ nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid{\isachardoublequote}}
-  with corresponding theorems
+  definition is propagated onto a global definition of \isa{{\isachardoublequote}pow{\isacharunderscore}nat\ {\isasymColon}\ nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid{\isachardoublequote}} with corresponding theorems
 
   \isa{pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}\isasep\isanewline%
 pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x}.
 
-  \noindent As you can see from this example, for local
-  definitions you may use any specification tool
-  which works together with locales, such as Krauss's recursive function package
+  \noindent As you can see from this example, for local definitions
+  you may use any specification tool which works together with
+  locales, such as Krauss's recursive function package
   \cite{krauss2006}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -833,19 +821,17 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-We introduced Isar classes by analogy to type classes in
-  functional programming;  if we reconsider this in the
-  context of what has been said about type classes and locales,
-  we can drive this analogy further by stating that type
-  classes essentially correspond to functors that have
-  a canonical interpretation as type classes.
-  There is also the possibility of other interpretations.
-  For example, \isa{list}s also form a monoid with
-  \isa{append} and \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it
-  seems inappropriate to apply to lists
-  the same operations as for genuinely algebraic types.
-  In such a case, we can simply make a particular interpretation
-  of monoids for lists:%
+We introduced Isar classes by analogy to type classes in functional
+  programming; if we reconsider this in the context of what has been
+  said about type classes and locales, we can drive this analogy
+  further by stating that type classes essentially correspond to
+  functors that have a canonical interpretation as type classes.
+  There is also the possibility of other interpretations.  For
+  example, \isa{list}s also form a monoid with \isa{append} and
+  \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it seems inappropriate to apply to
+  lists the same operations as for genuinely algebraic types.  In such
+  a case, we can simply make a particular interpretation of monoids
+  for lists:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -969,12 +955,10 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-The logical proof is carried out on the locale level.
-  Afterwards it is propagated
-  to the type system, making \isa{group} an instance of
-  \isa{monoid} by adding an additional edge
-  to the graph of subclass relations
-  (\figref{fig:subclass}).
+The logical proof is carried out on the locale level.  Afterwards it
+  is propagated to the type system, making \isa{group} an instance
+  of \isa{monoid} by adding an additional edge to the graph of
+  subclass relations (\figref{fig:subclass}).
 
   \begin{figure}[htbp]
    \begin{center}
@@ -1006,8 +990,7 @@
    \end{center}
   \end{figure}
 
-  For illustration, a derived definition
-  in \isa{group} using \isa{pow{\isacharunderscore}nat}%
+  For illustration, a derived definition in \isa{group} using \isa{pow{\isacharunderscore}nat}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1029,9 +1012,7 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent yields the global definition of
-  \isa{{\isachardoublequote}pow{\isacharunderscore}int\ {\isasymColon}\ int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequote}}
-  with the corresponding theorem \isa{pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{0}}\ {\isasymle}\ k\ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}}.%
+\noindent yields the global definition of \isa{{\isachardoublequote}pow{\isacharunderscore}int\ {\isasymColon}\ int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequote}} with the corresponding theorem \isa{pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{0}}\ {\isasymle}\ k\ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1040,9 +1021,9 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-As a convenience, class context syntax allows references
-  to local class operations and their global counterparts
-  uniformly;  type inference resolves ambiguities.  For example:%
+As a convenience, class context syntax allows references to local
+  class operations and their global counterparts uniformly; type
+  inference resolves ambiguities.  For example:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1082,11 +1063,11 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent Here in example 1, the term refers to the local class operation
-  \isa{mult\ {\isacharbrackleft}{\isasymalpha}{\isacharbrackright}}, whereas in example 2 the type constraint
-  enforces the global class operation \isa{mult\ {\isacharbrackleft}nat{\isacharbrackright}}.
-  In the global context in example 3, the reference is
-  to the polymorphic global class operation \isa{mult\ {\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isasymColon}\ semigroup{\isacharbrackright}}.%
+\noindent Here in example 1, the term refers to the local class
+  operation \isa{mult\ {\isacharbrackleft}{\isasymalpha}{\isacharbrackright}}, whereas in example 2 the type
+  constraint enforces the global class operation \isa{mult\ {\isacharbrackleft}nat{\isacharbrackright}}.
+  In the global context in example 3, the reference is to the
+  polymorphic global class operation \isa{mult\ {\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isasymColon}\ semigroup{\isacharbrackright}}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1099,16 +1080,13 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Turning back to the first motivation for type classes,
-  namely overloading, it is obvious that overloading
-  stemming from \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} statements and
-  \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}
-  targets naturally maps to Haskell type classes.
-  The code generator framework \cite{isabelle-codegen} 
-  takes this into account.  If the target language (e.g.~SML)
-  lacks type classes, then they
-  are implemented by an explicit dictionary construction.
-  As example, let's go back to the power function:%
+Turning back to the first motivation for type classes, namely
+  overloading, it is obvious that overloading stemming from \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} statements and \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} targets naturally
+  maps to Haskell type classes.  The code generator framework
+  \cite{isabelle-codegen} takes this into account.  If the target
+  language (e.g.~SML) lacks type classes, then they are implemented by
+  an explicit dictionary construction.  As example, let's go back to
+  the power function:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1328,13 +1306,121 @@
 %
 \endisadelimquote
 %
+\begin{isamarkuptext}%
+\noindent In Scala, implicts are used as dictionaries:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\isataginvisible
+%
+\endisataginvisible
+{\isafoldinvisible}%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isatypewriter%
+\noindent%
+\hspace*{0pt}object Example {\char123}\\
+\hspace*{0pt}\\
+\hspace*{0pt}import /*implicits*/ Example.semigroup{\char95}int,~Example.monoidl{\char95}int,\\
+\hspace*{0pt} ~Example.monoid{\char95}int,~Example.group{\char95}int\\
+\hspace*{0pt}\\
+\hspace*{0pt}abstract sealed class nat\\
+\hspace*{0pt}final case object Zero{\char95}nat extends nat\\
+\hspace*{0pt}final case class Suc(a:~nat) extends nat\\
+\hspace*{0pt}\\
+\hspace*{0pt}def nat{\char95}aux(i:~BigInt,~n:~nat):~nat =\\
+\hspace*{0pt} ~(if (i <= BigInt(0)) n else nat{\char95}aux(i - BigInt(1),~Suc(n)))\\
+\hspace*{0pt}\\
+\hspace*{0pt}def nat(i:~BigInt):~nat = nat{\char95}aux(i,~Zero{\char95}nat)\\
+\hspace*{0pt}\\
+\hspace*{0pt}trait semigroup[A] {\char123}\\
+\hspace*{0pt} ~val `Example+mult`:~(A,~A) => A\\
+\hspace*{0pt}{\char125}\\
+\hspace*{0pt}def mult[A](a:~A,~b:~A)(implicit A:~semigroup[A]):~A =\\
+\hspace*{0pt} ~A.`Example+mult`(a,~b)\\
+\hspace*{0pt}\\
+\hspace*{0pt}trait monoidl[A] extends semigroup[A] {\char123}\\
+\hspace*{0pt} ~val `Example+neutral`:~A\\
+\hspace*{0pt}{\char125}\\
+\hspace*{0pt}def neutral[A](implicit A:~monoidl[A]):~A = A.`Example+neutral`\\
+\hspace*{0pt}\\
+\hspace*{0pt}trait monoid[A] extends monoidl[A] {\char123}\\
+\hspace*{0pt}{\char125}\\
+\hspace*{0pt}\\
+\hspace*{0pt}trait group[A] extends monoid[A] {\char123}\\
+\hspace*{0pt} ~val `Example+inverse`:~A => A\\
+\hspace*{0pt}{\char125}\\
+\hspace*{0pt}def inverse[A](a:~A)(implicit A:~group[A]):~A = A.`Example+inverse`(a)\\
+\hspace*{0pt}\\
+\hspace*{0pt}def pow{\char95}nat[A:~monoid](xa0:~nat,~x:~A):~A = (xa0,~x) match {\char123}\\
+\hspace*{0pt} ~case (Zero{\char95}nat,~x) => neutral[A]\\
+\hspace*{0pt} ~case (Suc(n),~x) => mult[A](x,~pow{\char95}nat[A](n,~x))\\
+\hspace*{0pt}{\char125}\\
+\hspace*{0pt}\\
+\hspace*{0pt}def pow{\char95}int[A:~group](k:~BigInt,~x:~A):~A =\\
+\hspace*{0pt} ~(if (BigInt(0) <= k) pow{\char95}nat[A](nat(k),~x)\\
+\hspace*{0pt} ~~~else inverse[A](pow{\char95}nat[A](nat((- k)),~x)))\\
+\hspace*{0pt}\\
+\hspace*{0pt}def mult{\char95}int(i:~BigInt,~j:~BigInt):~BigInt = i + j\\
+\hspace*{0pt}\\
+\hspace*{0pt}implicit def semigroup{\char95}int:~semigroup[BigInt] = new semigroup[BigInt] {\char123}\\
+\hspace*{0pt} ~val `Example+mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\
+\hspace*{0pt}{\char125}\\
+\hspace*{0pt}\\
+\hspace*{0pt}def neutral{\char95}int:~BigInt = BigInt(0)\\
+\hspace*{0pt}\\
+\hspace*{0pt}implicit def monoidl{\char95}int:~monoidl[BigInt] = new monoidl[BigInt] {\char123}\\
+\hspace*{0pt} ~val `Example+neutral` = neutral{\char95}int\\
+\hspace*{0pt} ~val `Example+mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\
+\hspace*{0pt}{\char125}\\
+\hspace*{0pt}\\
+\hspace*{0pt}implicit def monoid{\char95}int:~monoid[BigInt] = new monoid[BigInt] {\char123}\\
+\hspace*{0pt} ~val `Example+neutral` = neutral{\char95}int\\
+\hspace*{0pt} ~val `Example+mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\
+\hspace*{0pt}{\char125}\\
+\hspace*{0pt}\\
+\hspace*{0pt}def inverse{\char95}int(i:~BigInt):~BigInt = (- i)\\
+\hspace*{0pt}\\
+\hspace*{0pt}implicit def group{\char95}int:~group[BigInt] = new group[BigInt] {\char123}\\
+\hspace*{0pt} ~val `Example+inverse` = (a:~BigInt) => inverse{\char95}int(a)\\
+\hspace*{0pt} ~val `Example+neutral` = neutral{\char95}int\\
+\hspace*{0pt} ~val `Example+mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\
+\hspace*{0pt}{\char125}\\
+\hspace*{0pt}\\
+\hspace*{0pt}def example:~BigInt = pow{\char95}int[BigInt](BigInt(10),~BigInt(- 2))\\
+\hspace*{0pt}\\
+\hspace*{0pt}{\char125}~/* object Example */%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
 \isamarkupsubsection{Inspecting the type class universe%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-To facilitate orientation in complex subclass structures,
-  two diagnostics commands are provided:
+To facilitate orientation in complex subclass structures, two
+  diagnostics commands are provided:
 
   \begin{description}
 
diff -r abe92b33ac9f -r d0196406ee32 doc-src/Codegen/Thy/Inductive_Predicate.thy
--- a/doc-src/Codegen/Thy/Inductive_Predicate.thy	Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/Codegen/Thy/Inductive_Predicate.thy	Fri Aug 27 14:25:29 2010 +0200
@@ -7,7 +7,7 @@
 
 inductive %invisible append where
   "append [] ys ys"
-| "append xs ys zs ==> append (x # xs) ys (x # zs)"
+| "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
 
 lemma %invisible append: "append xs ys zs = (xs @ ys = zs)"
   by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros)
@@ -95,9 +95,9 @@
   "append_i_i_o"}).  You can specify your own names as follows:
 *}
 
-code_pred %quote (modes: i => i => o => bool as concat,
-  o => o => i => bool as split,
-  i => o => i => bool as suffix) append .
+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 *}
 
@@ -220,8 +220,8 @@
   "values"} and the number of elements.
 *}
 
-values %quote [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
-values %quote [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
+values %quote [mode: i \<Rightarrow> o \<Rightarrow> bool] 20 "{n. tranclp succ 10 n}"
+values %quote [mode: o \<Rightarrow> i \<Rightarrow> bool] 10 "{n. tranclp succ n 10}"
 
 
 subsection {* Embedding into functional code within Isabelle/HOL *}
diff -r abe92b33ac9f -r d0196406ee32 doc-src/Codegen/Thy/Introduction.thy
--- a/doc-src/Codegen/Thy/Introduction.thy	Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/Codegen/Thy/Introduction.thy	Fri Aug 27 14:25:29 2010 +0200
@@ -8,8 +8,9 @@
   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
-  languages @{text SML} \cite{SML}, @{text OCaml} \cite{OCaml} and
-  @{text Haskell} \cite{haskell-revised-report}.
+  languages @{text SML} \cite{SML}, @{text OCaml} \cite{OCaml},
+  @{text Haskell} \cite{haskell-revised-report} and @{text Scala}
+  \cite{scala-overview-tech-report}.
 
   To profit from this tutorial, some familiarity and experience with
   @{theory HOL} \cite{isa-tutorial} and its basic theories is assumed.
@@ -78,8 +79,8 @@
   target language identifier and a freely chosen module name.  A file
   name denotes the destination to store the generated code.  Note that
   the semantics of the destination depends on the target language: for
-  @{text SML} and @{text OCaml} it denotes a \emph{file}, for @{text
-  Haskell} it denotes a \emph{directory} where a file named as the
+  @{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:
 *}
 
diff -r abe92b33ac9f -r d0196406ee32 doc-src/Codegen/Thy/document/Adaptation.tex
--- a/doc-src/Codegen/Thy/document/Adaptation.tex	Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex	Fri Aug 27 14:25:29 2010 +0200
@@ -240,7 +240,7 @@
 \hspace*{0pt}structure Example :~sig\\
 \hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
 \hspace*{0pt} ~datatype boola = True | False\\
-\hspace*{0pt} ~val anda :~boola -> boola -> boola\\
+\hspace*{0pt} ~val conj :~boola -> boola -> boola\\
 \hspace*{0pt} ~val less{\char95}nat :~nat -> nat -> boola\\
 \hspace*{0pt} ~val less{\char95}eq{\char95}nat :~nat -> nat -> boola\\
 \hspace*{0pt} ~val in{\char95}interval :~nat * nat -> nat -> boola\\
@@ -250,17 +250,17 @@
 \hspace*{0pt}\\
 \hspace*{0pt}datatype boola = True | False;\\
 \hspace*{0pt}\\
-\hspace*{0pt}fun anda p True = p\\
-\hspace*{0pt} ~| anda p False = False\\
-\hspace*{0pt} ~| anda True p = p\\
-\hspace*{0pt} ~| anda False p = False;\\
+\hspace*{0pt}fun conj p True = p\\
+\hspace*{0pt} ~| conj p False = False\\
+\hspace*{0pt} ~| conj True p = p\\
+\hspace*{0pt} ~| conj False p = 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}fun in{\char95}interval (k,~l) n = conj (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\
 \hspace*{0pt}\\
 \hspace*{0pt}end;~(*struct Example*)%
 \end{isamarkuptext}%
diff -r abe92b33ac9f -r d0196406ee32 doc-src/Codegen/Thy/document/Inductive_Predicate.tex
--- a/doc-src/Codegen/Thy/document/Inductive_Predicate.tex	Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Inductive_Predicate.tex	Fri Aug 27 14:25:29 2010 +0200
@@ -212,9 +212,9 @@
 %
 \isatagquote
 \isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
-\ {\isacharparenleft}modes{\isacharcolon}\ i\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ bool\ as\ concat{\isacharcomma}\isanewline
-\ \ o\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool\ as\ split{\isacharcomma}\isanewline
-\ \ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool\ as\ suffix{\isacharparenright}\ append\ \isacommand{{\isachardot}}\isamarkupfalse%
+\ {\isacharparenleft}modes{\isacharcolon}\ i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool\ as\ concat{\isacharcomma}\isanewline
+\ \ o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool\ as\ split{\isacharcomma}\isanewline
+\ \ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool\ as\ suffix{\isacharparenright}\ append\ \isacommand{{\isachardot}}\isamarkupfalse%
 %
 \endisatagquote
 {\isafoldquote}%
@@ -422,9 +422,9 @@
 %
 \isatagquote
 \isacommand{values}\isamarkupfalse%
-\ {\isacharbrackleft}mode{\isacharcolon}\ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ bool{\isacharbrackright}\ {\isadigit{2}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
+\ {\isacharbrackleft}mode{\isacharcolon}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool{\isacharbrackright}\ {\isadigit{2}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
 \isacommand{values}\isamarkupfalse%
-\ {\isacharbrackleft}mode{\isacharcolon}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool{\isacharbrackright}\ {\isadigit{1}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ n\ {\isadigit{1}}{\isadigit{0}}{\isacharbraceright}{\isachardoublequoteclose}%
+\ {\isacharbrackleft}mode{\isacharcolon}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool{\isacharbrackright}\ {\isadigit{1}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ n\ {\isadigit{1}}{\isadigit{0}}{\isacharbraceright}{\isachardoublequoteclose}%
 \endisatagquote
 {\isafoldquote}%
 %
diff -r abe92b33ac9f -r d0196406ee32 doc-src/Codegen/Thy/document/Introduction.tex
--- a/doc-src/Codegen/Thy/document/Introduction.tex	Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex	Fri Aug 27 14:25:29 2010 +0200
@@ -25,8 +25,9 @@
 \begin{isamarkuptext}%
 This tutorial introduces the code generator facilities of \isa{Isabelle{\isacharslash}HOL}.  It allows to turn (a certain class of) HOL
   specifications into corresponding executable code in the programming
-  languages \isa{SML} \cite{SML}, \isa{OCaml} \cite{OCaml} and
-  \isa{Haskell} \cite{haskell-revised-report}.
+  languages \isa{SML} \cite{SML}, \isa{OCaml} \cite{OCaml},
+  \isa{Haskell} \cite{haskell-revised-report} and \isa{Scala}
+  \cite{scala-overview-tech-report}.
 
   To profit from this tutorial, some familiarity and experience with
   \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \cite{isa-tutorial} and its basic theories is assumed.%
@@ -191,7 +192,8 @@
   target language identifier and a freely chosen module name.  A file
   name denotes the destination to store the generated code.  Note that
   the semantics of the destination depends on the target language: for
-  \isa{SML} and \isa{OCaml} it denotes a \emph{file}, for \isa{Haskell} it denotes a \emph{directory} where a file named as the
+  \isa{SML}, \isa{OCaml} and \isa{Scala} it denotes a \emph{file},
+  for \isa{Haskell} it denotes a \emph{directory} where a file named as the
   module name (with extension \isa{{\isachardot}hs}) is written:%
 \end{isamarkuptext}%
 \isamarkuptrue%
diff -r abe92b33ac9f -r d0196406ee32 doc-src/Codegen/Thy/pictures/architecture.tex
--- a/doc-src/Codegen/Thy/pictures/architecture.tex	Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/Codegen/Thy/pictures/architecture.tex	Fri Aug 27 14:25:29 2010 +0200
@@ -30,8 +30,8 @@
   \node (seri) at (1.5, 0) [process, positive] {serialisation};
   \node (SML) at (2.5, 3) [entity, positive] {\sys{SML}};
   \node (OCaml) at (2.5, 2) [entity, positive] {\sys{OCaml}};
-  \node (further) at (2.5, 1) [entity, positive] {(\ldots)};
-  \node (Haskell) at (2.5, 0) [entity, positive] {\sys{Haskell}};
+  \node (Haskell) at (2.5, 1) [entity, positive] {\sys{Haskell}};
+  \node (Scala) at (2.5, 0) [entity, positive] {\sys{Scala}};
   \draw [semithick] (spec) -- (spec_user_join);
   \draw [semithick] (user) -- (spec_user_join);
   \draw [-diamond, semithick] (spec_user_join) -- (raw);
@@ -41,8 +41,8 @@
   \draw [arrow] (iml) -- (seri);
   \draw [arrow] (seri) -- (SML);
   \draw [arrow] (seri) -- (OCaml);
-  \draw [arrow, dashed] (seri) -- (further);
   \draw [arrow] (seri) -- (Haskell);
+  \draw [arrow] (seri) -- (Scala);
 \end{tikzpicture}
 
 }
diff -r abe92b33ac9f -r d0196406ee32 doc-src/Codegen/codegen.tex
--- a/doc-src/Codegen/codegen.tex	Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/Codegen/codegen.tex	Fri Aug 27 14:25:29 2010 +0200
@@ -22,7 +22,7 @@
 \begin{abstract}
   \noindent This tutorial introduces the code generator facilities of Isabelle/HOL.
     They empower the user to turn HOL specifications into corresponding executable
-    programs in the languages SML, OCaml and Haskell.
+    programs in the languages SML, OCaml, Haskell and Scala.
 \end{abstract}
 
 \thispagestyle{empty}\clearpage
diff -r abe92b33ac9f -r d0196406ee32 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Aug 27 14:25:29 2010 +0200
@@ -968,7 +968,8 @@
 
   \medskip One framework generates code from functional programs
   (including overloading using type classes) to SML \cite{SML}, OCaml
-  \cite{OCaml} and Haskell \cite{haskell-revised-report}.
+  \cite{OCaml}, Haskell \cite{haskell-revised-report} and Scala
+  \cite{scala-overview-tech-report}.
   Conceptually, code generation is split up in three steps:
   \emph{selection} of code theorems, \emph{translation} into an
   abstract executable view and \emph{serialization} to a specific
@@ -1015,7 +1016,7 @@
     class: nameref
     ;
 
-    target: 'OCaml' | 'SML' | 'Haskell'
+    target: 'SML' | 'OCaml' | 'Haskell' | 'Scala'
     ;
 
     'code' ( 'del' | 'abstype' | 'abstract' ) ?
@@ -1088,7 +1089,7 @@
   after the @{keyword "module_name"} keyword; then \emph{all} code is
   placed in this module.
 
-  For \emph{SML} and \emph{OCaml}, the file specification refers to a
+  For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification refers to a
   single file; for \emph{Haskell}, it refers to a whole directory,
   where code is generated in multiple files reflecting the module
   hierarchy.  Omitting the file specification denotes standard
diff -r abe92b33ac9f -r d0196406ee32 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Aug 27 14:25:29 2010 +0200
@@ -984,7 +984,8 @@
 
   \medskip One framework generates code from functional programs
   (including overloading using type classes) to SML \cite{SML}, OCaml
-  \cite{OCaml} and Haskell \cite{haskell-revised-report}.
+  \cite{OCaml}, Haskell \cite{haskell-revised-report} and Scala
+  \cite{scala-overview-tech-report}.
   Conceptually, code generation is split up in three steps:
   \emph{selection} of code theorems, \emph{translation} into an
   abstract executable view and \emph{serialization} to a specific
@@ -1031,7 +1032,7 @@
     class: nameref
     ;
 
-    target: 'OCaml' | 'SML' | 'Haskell'
+    target: 'SML' | 'OCaml' | 'Haskell' | 'Scala'
     ;
 
     'code' ( 'del' | 'abstype' | 'abstract' ) ?
@@ -1103,7 +1104,7 @@
   after the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} keyword; then \emph{all} code is
   placed in this module.
 
-  For \emph{SML} and \emph{OCaml}, the file specification refers to a
+  For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification refers to a
   single file; for \emph{Haskell}, it refers to a whole directory,
   where code is generated in multiple files reflecting the module
   hierarchy.  Omitting the file specification denotes standard
diff -r abe92b33ac9f -r d0196406ee32 doc-src/manual.bib
--- a/doc-src/manual.bib	Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/manual.bib	Fri Aug 27 14:25:29 2010 +0200
@@ -984,6 +984,14 @@
 
 %O
 
+@TechReport{scala-overview-tech-report,
+  author =       {Martin Odersky and al.},
+  title =        {An Overview of the Scala Programming Language},
+  institution =  {EPFL Lausanne, Switzerland},
+  year =         2004,
+  number =       {IC/2004/64}
+}
+
 @Manual{pvs-language,
   title		= {The {PVS} specification language},
   author	= {S. Owre and N. Shankar and J. M. Rushby},
diff -r abe92b33ac9f -r d0196406ee32 src/HOL/Library/Code_Natural.thy
--- a/src/HOL/Library/Code_Natural.thy	Fri Aug 27 12:57:55 2010 +0200
+++ b/src/HOL/Library/Code_Natural.thy	Fri Aug 27 14:25:29 2010 +0200
@@ -9,7 +9,9 @@
 section {* Alternative representation of @{typ code_numeral} for @{text Haskell} and @{text Scala} *}
 
 code_include Haskell "Natural"
-{*newtype Natural = Natural Integer deriving (Eq, Show, Read);
+{*import Data.Array.ST;
+
+newtype Natural = Natural Integer deriving (Eq, Show, Read);
 
 instance Num Natural where {
   fromInteger k = Natural (if k >= 0 then k else 0);
@@ -50,6 +52,7 @@
     | otherwise = (Natural k, Natural l) where (k, l) = quotRem n m;
 };*}
 
+
 code_reserved Haskell Natural
 
 code_include Scala "Natural"
diff -r abe92b33ac9f -r d0196406ee32 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Fri Aug 27 12:57:55 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Fri Aug 27 14:25:29 2010 +0200
@@ -27,7 +27,6 @@
 fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved
     args_num is_singleton_constr (deresolve, deresolve_full) =
   let
-    val deresolve_base = Long_Name.base_name o deresolve;
     fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
     fun intro_tyvars vs = intro_vars (map (first_upper o fst) vs);
     fun print_tyco_expr tyvars fxy (tyco, tys) = applify "[" "]"
@@ -135,7 +134,7 @@
     fun print_context tyvars vs name = applify "[" "]"
       (fn (v, sort) => (Pretty.block o map str)
         (lookup_tyvar tyvars v :: maps (fn sort => [": ", deresolve sort]) sort))
-          NOBR ((str o deresolve_base) name) vs;
+          NOBR ((str o deresolve) name) vs;
     fun print_defhead tyvars vars name vs params tys ty =
       Pretty.block [str "def ", constraint (applify "(" ")" (fn (param, ty) =>
         constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
@@ -202,22 +201,22 @@
           let
             val tyvars = intro_tyvars vs reserved;
             fun print_co ((co, _), []) =
-                  concat [str "final", str "case", str "object", (str o deresolve_base) co,
-                    str "extends", applify "[" "]" I NOBR ((str o deresolve_base) name)
+                  concat [str "final", str "case", str "object", (str o deresolve) co,
+                    str "extends", applify "[" "]" I NOBR ((str o deresolve) name)
                       (replicate (length vs) (str "Nothing"))]
               | print_co ((co, vs_args), tys) =
                   concat [applify "(" ")"
                     (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg)) NOBR
                     (applify "[" "]" (str o lookup_tyvar tyvars) NOBR ((concat o map str)
-                      ["final", "case", "class", deresolve_base co]) vs_args)
+                      ["final", "case", "class", deresolve co]) vs_args)
                     (Name.names (snd reserved) "a" tys),
                     str "extends",
                     applify "[" "]" (str o lookup_tyvar tyvars o fst) NOBR
-                      ((str o deresolve_base) name) vs
+                      ((str o deresolve) name) vs
                   ];
           in
             Pretty.chunks (applify "[" "]" (str o prefix "+" o lookup_tyvar tyvars o fst)
-              NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_base name]) vs
+              NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve name]) vs
                 :: map print_co cos)
           end
       | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
@@ -241,7 +240,7 @@
               in
                 concat [str "def", constraint (Pretty.block [applify "(" ")"
                   (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
-                  (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_base classparam))
+                  (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve classparam))
                   (auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
                   add_typarg (deresolve name), str ")"]) (print_typ tyvars NOBR ty), str "=",
                   applify "(" ")" (str o lookup_var vars) NOBR
@@ -250,7 +249,7 @@
           in
             Pretty.chunks (
               (Pretty.block_enclose
-                (concat ([str "trait", (add_typarg o deresolve_base) name]
+                (concat ([str "trait", (add_typarg o deresolve) name]
                   @ the_list (print_super_classes super_classes) @ [str "{"]), str "}")
                 (map print_classparam_val classparams))
               :: map print_classparam_def classparams
@@ -289,7 +288,7 @@
 datatype node =
     Dummy
   | Stmt of Code_Thingol.stmt
-  | Module of ((Name.context * Name.context) * Name.context) * (string list * (string * node) Graph.T);
+  | Module of (string list * (string * node) Graph.T);
 
 in
 
@@ -307,29 +306,53 @@
     val dest_name = Code_Printer.dest_name #>> (the o Symtab.lookup fragments_tab);
 
     (* building empty module hierarchy *)
-    val empty_module = (((reserved, reserved), reserved), ([], Graph.empty));
+    val empty_module = ([], Graph.empty);
     fun map_module f (Module content) = Module (f content);
-    fun declare_module name_fragement ((nsp_class, nsp_object), nsp_common) =
-      let
-        val declare = Name.declare name_fragement;
-      in ((declare nsp_class, declare nsp_object), declare nsp_common) end;
-    fun ensure_module name_fragement (nsps, (implicits, nodes)) =
-      if can (Graph.get_node nodes) name_fragement then (nsps, (implicits, nodes))
-      else
-        (nsps |> declare_module name_fragement, (implicits,
-          nodes |> Graph.new_node (name_fragement, (name_fragement, Module empty_module))));
+    fun change_module [] = I
+      | change_module (name_fragment :: name_fragments) =
+          apsnd o Graph.map_node name_fragment o apsnd o map_module
+            o change_module name_fragments;
+    fun ensure_module name_fragment (implicits, nodes) =
+      if can (Graph.get_node nodes) name_fragment then (implicits, nodes)
+      else (implicits,
+        nodes |> Graph.new_node (name_fragment, (name_fragment, Module empty_module)));
     fun allocate_module [] = I
       | allocate_module (name_fragment :: name_fragments) =
           ensure_module name_fragment
-          #> (apsnd o apsnd o Graph.map_node name_fragment o apsnd o map_module o allocate_module) name_fragments;
+          #> (apsnd o Graph.map_node name_fragment o apsnd o map_module o allocate_module) name_fragments;
     val empty_program = Symtab.fold (fn (_, fragments) => allocate_module fragments)
       fragments_tab empty_module;
-    fun change_module [] = I
-      | change_module (name_fragment :: name_fragments) =
-          apsnd o apsnd o Graph.map_node name_fragment o apsnd o map_module
-            o change_module name_fragments;
 
-    (* statement declaration *)
+    (* distribute statements over hierarchy *)
+    fun add_stmt name stmt =
+      let
+        val (name_fragments, base) = dest_name name;
+        fun is_classinst stmt = case stmt
+         of Code_Thingol.Classinst _ => true
+          | _ => false;
+        val implicit_deps = filter (is_classinst o Graph.get_node program)
+          (Graph.imm_succs program name);
+      in
+        change_module name_fragments (fn (implicits, nodes) =>
+          (union (op =) implicit_deps implicits, Graph.new_node (name, (base, Stmt stmt)) nodes))
+      end;
+    fun add_dependency name name' =
+      let
+        val (name_fragments, base) = dest_name name;
+        val (name_fragments', base') = dest_name name';
+        val (name_fragments_common, (diff, diff')) =
+          chop_prefix (op =) (name_fragments, name_fragments');
+        val dep = if null diff then (name, name') else (hd diff, hd diff')
+      in (change_module name_fragments_common o apsnd) (Graph.add_edge dep) end;
+    val proto_program = empty_program
+      |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
+      |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
+
+    (* name declarations *)
+    fun namify_module name_fragment ((nsp_class, nsp_object), nsp_common) =
+      let
+        val declare = Name.declare name_fragment;
+      in (name_fragment, ((declare nsp_class, declare nsp_object), declare nsp_common)) end;
     fun namify_class base ((nsp_class, nsp_object), nsp_common) =
       let
         val (base', nsp_class') = yield_singleton Name.variants base nsp_class
@@ -346,70 +369,58 @@
         (base',
           ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
       end;
-    fun declare_stmt name stmt =
+    fun namify_stmt (Code_Thingol.Fun _) = namify_object
+      | namify_stmt (Code_Thingol.Datatype _) = namify_class
+      | namify_stmt (Code_Thingol.Datatypecons _) = namify_common true
+      | namify_stmt (Code_Thingol.Class _) = namify_class
+      | namify_stmt (Code_Thingol.Classrel _) = namify_object
+      | namify_stmt (Code_Thingol.Classparam _) = namify_object
+      | namify_stmt (Code_Thingol.Classinst _) = namify_common false;
+    fun make_declarations nsps (implicits, nodes) =
       let
-        val (name_fragments, base) = dest_name name;
-        val namify = case stmt
-         of Code_Thingol.Fun _ => namify_object
-          | Code_Thingol.Datatype _ => namify_class
-          | Code_Thingol.Datatypecons _ => namify_common true
-          | Code_Thingol.Class _ => namify_class
-          | Code_Thingol.Classrel _ => namify_object
-          | Code_Thingol.Classparam _ => namify_object
-          | Code_Thingol.Classinst _ => namify_common false;
-        val stmt' = case stmt
-         of Code_Thingol.Datatypecons _ => Dummy
-          | Code_Thingol.Classrel _ => Dummy
-          | Code_Thingol.Classparam _ => Dummy
-          | _ => Stmt stmt;
-        fun is_classinst stmt = case stmt
-         of Code_Thingol.Classinst _ => true
-          | _ => false;
-        val implicit_deps = filter (is_classinst o Graph.get_node program)
-          (Graph.imm_succs program name);
-        fun declaration (nsps, (implicits, nodes)) =
+        val (module_fragments, stmt_names) = List.partition
+          (fn name_fragment => case Graph.get_node nodes name_fragment
+            of (_, Module _) => true | _ => false) (Graph.keys nodes);
+        fun modify_stmt (Stmt (Code_Thingol.Datatypecons _)) = Dummy
+          | modify_stmt (Stmt (Code_Thingol.Classrel _)) = Dummy
+          | modify_stmt (Stmt (Code_Thingol.Classparam _)) = Dummy
+          | modify_stmt stmt = stmt;
+        fun declare namify modify name (nsps, nodes) =
           let
-            val (base', nsps') = namify base nsps;
-            val implicits' = union (op =) implicit_deps implicits;
-            val nodes' = Graph.new_node (name, (base', stmt')) nodes;
-          in (nsps', (implicits', nodes')) end;
-      in change_module name_fragments declaration end;
-
-    (* dependencies *)
-    fun add_dependency name name' =
-      let
-        val (name_fragments, base) = dest_name name;
-        val (name_fragments', base') = dest_name name';
-        val (name_fragments_common, (diff, diff')) =
-          chop_prefix (op =) (name_fragments, name_fragments');
-        val dep = if null diff then (name, name') else (hd diff, hd diff')
-      in (change_module name_fragments_common o apsnd o apsnd) (Graph.add_edge dep) end;
-
-    (* producing program *)
-    val (_, (_, sca_program)) = empty_program
-      |> Graph.fold (fn (name, (stmt, _)) => declare_stmt name stmt) program
-      |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
+            val (base, node) = Graph.get_node nodes name;
+            val (base', nsps') = namify node base nsps;
+            val nodes' = Graph.map_node name (K (base', modify node)) nodes;
+          in (nsps', nodes') end;
+        val (nsps', nodes') = (nsps, nodes)
+          |> fold (declare (K namify_module) I) module_fragments
+          |> fold (declare (namify_stmt o (fn Stmt stmt => stmt)) modify_stmt) stmt_names;
+        val nodes'' = nodes'
+          |> fold (fn name_fragment => (Graph.map_node name_fragment
+              o apsnd o map_module) (make_declarations nsps')) module_fragments;
+      in (implicits, nodes'') end;
+    val (_, sca_program) = make_declarations ((reserved, reserved), reserved) proto_program;
 
     (* deresolving *)
-    fun deresolve name =
+    fun deresolver prefix_fragments name =
       let
         val (name_fragments, _) = dest_name name;
-        val nodes = fold (fn name_fragement => fn nodes => case Graph.get_node nodes name_fragement
-         of (_, Module (_, (_, nodes))) => nodes) name_fragments sca_program;
+        val (_, (_, remainder)) = chop_prefix (op =) (prefix_fragments, name_fragments);
+        val nodes = fold (fn name_fragment => fn nodes => case Graph.get_node nodes name_fragment
+         of (_, Module (_, nodes)) => nodes) name_fragments sca_program;
         val (base', _) = Graph.get_node nodes name;
-      in Long_Name.implode (name_fragments @ [base']) end
+      in Long_Name.implode (remainder @ [base']) end
         handle Graph.UNDEF _ => error ("Unknown statement name: " ^ labelled_name name);
 
-  in (deresolve, sca_program) end;
+  in (deresolver, sca_program) end;
 
 fun serialize_scala labelled_name raw_reserved includes module_alias
     _ syntax_tyco syntax_const (code_of_pretty, code_writeln)
     program (stmt_names, presentation_stmt_names) destination =
   let
 
-    (* preprocess program *)
+    (* build program *)
     val reserved = fold (insert (op =) o fst) includes raw_reserved;
-    val (deresolve, sca_program) = scala_program_of_program labelled_name
+    val (deresolver, sca_program) = scala_program_of_program labelled_name
       (Name.make_context reserved) module_alias program;
 
     (* print statements *)
@@ -430,41 +441,44 @@
      of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
       | _ => false;
     val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
-      (make_vars reserved) args_num is_singleton_constr
-      (deresolve, Long_Name.implode o fst o split_last o Long_Name.explode (*FIXME full*));
+      (make_vars reserved) args_num is_singleton_constr;
 
     (* print nodes *)
-    fun print_implicit implicit =
+    fun print_implicit prefix_fragments implicit =
       let
-        val s = deresolve implicit;
+        val s = deresolver prefix_fragments implicit;
       in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
-    fun print_implicits implicits = case map_filter print_implicit implicits
-     of [] => NONE
-      | ps => (SOME o Pretty.block)
-          (str "import /*implicits*/" :: Pretty.brk 1 :: commas ps);
-    fun print_module base implicits p = Pretty.chunks2
-      ([str ("object " ^ base ^ " {")] @ the_list (print_implicits implicits)
+    fun print_implicits prefix_fragments implicits =
+      case map_filter (print_implicit prefix_fragments) implicits
+       of [] => NONE
+        | ps => (SOME o Pretty.block)
+            (str "import /*implicits*/" :: Pretty.brk 1 :: commas ps);
+    fun print_module prefix_fragments base implicits p = Pretty.chunks2
+      ([str ("object " ^ base ^ " {")] @ the_list (print_implicits prefix_fragments implicits)
         @ [p, str ("} /* object " ^ base ^ " */")]);
-    fun print_node (_, Dummy) = NONE
-      | print_node (name, Stmt stmt) = if null presentation_stmt_names
+    fun print_node _ (_, Dummy) = NONE
+      | print_node prefix_fragments (name, Stmt stmt) =
+          if null presentation_stmt_names
           orelse member (op =) presentation_stmt_names name
-          then SOME (print_stmt (name, stmt))
+          then SOME (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt))
           else NONE
-      | print_node (name, Module (_, (implicits, nodes))) = if null presentation_stmt_names
-          then case print_nodes nodes
+      | print_node prefix_fragments (name_fragment, Module (implicits, nodes)) =
+          if null presentation_stmt_names
+          then case print_nodes (prefix_fragments @ [name_fragment]) nodes
            of NONE => NONE
-            | SOME p => SOME (print_module (Long_Name.base_name name) implicits p)
-          else print_nodes nodes
-    and print_nodes nodes = let
-        val ps = map_filter (fn name => print_node (name,
+            | SOME p => SOME (print_module prefix_fragments
+                (Long_Name.base_name name_fragment) implicits p)
+          else print_nodes [] nodes
+    and print_nodes prefix_fragments nodes = let
+        val ps = map_filter (fn name => print_node prefix_fragments (name,
           snd (Graph.get_node nodes name)))
             ((rev o flat o Graph.strong_conn) nodes);
       in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
 
     (* serialization *)
     val p_includes = if null presentation_stmt_names
-      then map (fn (base, p) => print_module base [] p) includes else [];
-    val p = Pretty.chunks2 (p_includes @ the_list (print_nodes sca_program));
+      then map (fn (base, p) => print_module [] base [] p) includes else [];
+    val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
   in
     Code_Target.mk_serialization target
       (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)