--- a/doc-src/IsarRef/logics.tex Fri Jul 13 22:36:10 2007 +0200
+++ b/doc-src/IsarRef/logics.tex Mon Jul 16 09:29:00 2007 +0200
@@ -798,7 +798,7 @@
\begin{rail}
'code\_gen' ( constexpr + ) ? \\
- ( ( 'in' target ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?;
+ ( ( 'in' target ( 'to' string ) ? ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?;
'code\_thms' ( constexpr + ) ?;
@@ -864,6 +864,10 @@
by giving (``name.*''), or referring to \emph{all} executable
constants currently available (``*'').
+ By default, for each involved theory one corresponding name space module
+ is generated. Alternativly, a module name may be specified after the (``to'')
+ keyword; then \emph{all} code is placed in this module.
+
For \emph{SML} and \emph{OCaml}, 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.