1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Jul 08 16:41:57 2010 +0200
1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Jul 08 16:48:33 2010 +0200
1.3 @@ -1000,7 +1000,7 @@
1.4 \begin{rail}
1.5 'export\_code' ( constexpr + ) \\
1.6 ( ( 'in' target ( 'module\_name' string ) ? \\
1.7 - ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
1.8 + 'file' ( string | '-' ) ( '(' args ')' ) ?) + ) ?
1.9 ;
1.10
1.11 const: term
1.12 @@ -1092,8 +1092,7 @@
1.13 single file; for \emph{Haskell}, it refers to a whole directory,
1.14 where code is generated in multiple files reflecting the module
1.15 hierarchy. The file specification ``@{text "-"}'' denotes standard
1.16 - output. For \emph{SML}, omitting the file specification compiles
1.17 - code internally in the context of the current ML session.
1.18 + output.
1.19
1.20 Serializers take an optional list of arguments in parentheses. For
1.21 \emph{SML} and \emph{OCaml}, ``@{text no_signatures}`` omits