1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Aug 27 14:24:26 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Aug 27 14:25:07 2010 +0200
     1.3 @@ -968,7 +968,8 @@
     1.4  
     1.5    \medskip One framework generates code from functional programs
     1.6    (including overloading using type classes) to SML \cite{SML}, OCaml
     1.7 -  \cite{OCaml} and Haskell \cite{haskell-revised-report}.
     1.8 +  \cite{OCaml}, Haskell \cite{haskell-revised-report} and Scala
     1.9 +  \cite{scala-overview-tech-report}.
    1.10    Conceptually, code generation is split up in three steps:
    1.11    \emph{selection} of code theorems, \emph{translation} into an
    1.12    abstract executable view and \emph{serialization} to a specific
    1.13 @@ -1015,7 +1016,7 @@
    1.14      class: nameref
    1.15      ;
    1.16  
    1.17 -    target: 'OCaml' | 'SML' | 'Haskell'
    1.18 +    target: 'SML' | 'OCaml' | 'Haskell' | 'Scala'
    1.19      ;
    1.20  
    1.21      'code' ( 'del' | 'abstype' | 'abstract' ) ?
    1.22 @@ -1088,7 +1089,7 @@
    1.23    after the @{keyword "module_name"} keyword; then \emph{all} code is
    1.24    placed in this module.
    1.25  
    1.26 -  For \emph{SML} and \emph{OCaml}, the file specification refers to a
    1.27 +  For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification refers to a
    1.28    single file; for \emph{Haskell}, it refers to a whole directory,
    1.29    where code is generated in multiple files reflecting the module
    1.30    hierarchy.  Omitting the file specification denotes standard