--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Aug 27 14:22:33 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Aug 27 14:24:26 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