1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Dec 23 08:31:14 2009 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Dec 23 08:31:14 2009 +0100
     1.3 @@ -1139,7 +1139,7 @@
     1.4    \end{matharray}
     1.5  
     1.6    \begin{rail}
     1.7 -    'export\_code' ( constexpr + ) ? \\
     1.8 +    'export\_code' ( constexpr + ) \\
     1.9        ( ( 'in' target ( 'module\_name' string ) ? \\
    1.10          ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
    1.11      ;
    1.12 @@ -1216,10 +1216,8 @@
    1.13  
    1.14    \item @{command (HOL) "export_code"} is the canonical interface for
    1.15    generating and serializing code: for a given list of constants, code
    1.16 -  is generated for the specified target languages.  Abstract code is
    1.17 -  cached incrementally.  If no constant is given, the currently cached
    1.18 -  code is serialized.  If no serialization instruction is given, only
    1.19 -  abstract code is cached.
    1.20 +  is generated for the specified target languages.  If no serialization
    1.21 +  instruction is given, only abstract code is generated internally.
    1.22  
    1.23    Constants may be specified by giving them literally, referring to
    1.24    all executable contants within a certain theory by giving @{text
    1.25 @@ -1239,20 +1237,21 @@
    1.26    code internally in the context of the current ML session.
    1.27  
    1.28    Serializers take an optional list of arguments in parentheses.  For
    1.29 -  \emph{Haskell} a module name prefix may be given using the ``@{text
    1.30 +  \emph{SML} and \emph{OCaml}, ``@{text no_signatures}`` omits
    1.31 +  explicit module signatures.
    1.32 +  
    1.33 +  For \emph{Haskell} a module name prefix may be given using the ``@{text
    1.34    "root:"}'' argument; ``@{text string_classes}'' adds a ``@{verbatim
    1.35    "deriving (Read, Show)"}'' clause to each appropriate datatype
    1.36    declaration.
    1.37  
    1.38    \item @{command (HOL) "code_thms"} prints a list of theorems
    1.39    representing the corresponding program containing all given
    1.40 -  constants; if no constants are given, the currently cached code
    1.41 -  theorems are printed.
    1.42 +  constants.
    1.43  
    1.44    \item @{command (HOL) "code_deps"} visualizes dependencies of
    1.45    theorems representing the corresponding program containing all given
    1.46 -  constants; if no constants are given, the currently cached code
    1.47 -  theorems are visualized.
    1.48 +  constants.
    1.49  
    1.50    \item @{command (HOL) "code_datatype"} specifies a constructor set
    1.51    for a logical type.