diff -r e527a34bf69d -r f50f0802ba99 doc-src/Codegen/Thy/document/Introduction.tex
--- a/doc-src/Codegen/Thy/document/Introduction.tex	Fri Aug 27 14:22:33 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex	Fri Aug 27 14:24:26 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%