# HG changeset patch
# User haftmann
# Date 1278600513 -7200
# Node ID c7e15d59c58d656ad53b89c112dd81c58fec4349
# Parent  0af0d45257be947baaba74853542272b1e4fc14e
updated documentation

diff -r 0af0d45257be -r c7e15d59c58d doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Jul 08 16:41:57 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Jul 08 16:48:33 2010 +0200
@@ -1000,7 +1000,7 @@
   \begin{rail}
     'export\_code' ( constexpr + ) \\
       ( ( 'in' target ( 'module\_name' string ) ? \\
-        ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
+        'file' ( string | '-' ) ( '(' args ')' ) ?) + ) ?
     ;
 
     const: term
@@ -1092,8 +1092,7 @@
   single file; for \emph{Haskell}, it refers to a whole directory,
   where code is generated in multiple files reflecting the module
   hierarchy.  The file specification ``@{text "-"}'' denotes standard
-  output.  For \emph{SML}, omitting the file specification compiles
-  code internally in the context of the current ML session.
+  output.
 
   Serializers take an optional list of arguments in parentheses.  For
   \emph{SML} and \emph{OCaml}, ``@{text no_signatures}`` omits
diff -r 0af0d45257be -r c7e15d59c58d doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu Jul 08 16:41:57 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu Jul 08 16:48:33 2010 +0200
@@ -1016,7 +1016,7 @@
   \begin{rail}
     'export\_code' ( constexpr + ) \\
       ( ( 'in' target ( 'module\_name' string ) ? \\
-        ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
+        'file' ( string | '-' ) ( '(' args ')' ) ?) + ) ?
     ;
 
     const: term
@@ -1107,8 +1107,7 @@
   single file; for \emph{Haskell}, it refers to a whole directory,
   where code is generated in multiple files reflecting the module
   hierarchy.  The file specification ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' denotes standard
-  output.  For \emph{SML}, omitting the file specification compiles
-  code internally in the context of the current ML session.
+  output.
 
   Serializers take an optional list of arguments in parentheses.  For
   \emph{SML} and \emph{OCaml}, ``\isa{no{\isacharunderscore}signatures}`` omits