# HG changeset patch
# User haftmann
# Date 1184570940 -7200
# Node ID d36e3ffdb5ce59c6d998cd976ad6962257fb3321
# Parent  d67aac3992c37e4a968cb62d0ea3dd19fa105939
updated

diff -r d67aac3992c3 -r d36e3ffdb5ce doc-src/IsarRef/logics.tex
--- 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.