NEWS and documentation, including correction of long-overseen "*"
authorhaftmann
Sun Feb 23 10:44:57 2014 +0100 (2014-02-23)
changeset 55686e99ed112d303
parent 55685 3f8bdc5364a9
child 55687 78c83cd477c1
NEWS and documentation, including correction of long-overseen "*"
NEWS
src/Doc/IsarRef/HOL_Specific.thy
     1.1 --- a/NEWS	Sun Feb 23 10:33:43 2014 +0100
     1.2 +++ b/NEWS	Sun Feb 23 10:44:57 2014 +0100
     1.3 @@ -90,6 +90,8 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Code generator: minimize exported identifiers by default.
     1.8 +
     1.9  * Code generation for SML and OCaml: dropped arcane "no_signatures" option.
    1.10  
    1.11  * Simproc "finite_Collect" is no longer enabled by default, due to
     2.1 --- a/src/Doc/IsarRef/HOL_Specific.thy	Sun Feb 23 10:33:43 2014 +0100
     2.2 +++ b/src/Doc/IsarRef/HOL_Specific.thy	Sun Feb 23 10:44:57 2014 +0100
     2.3 @@ -2393,7 +2393,7 @@
     2.4    \end{matharray}
     2.5  
     2.6    @{rail \<open>
     2.7 -    @@{command (HOL) export_code} ( constexpr + ) \<newline>
     2.8 +    @@{command (HOL) export_code} ( @'open' ) ? ( constexpr + ) \<newline>
     2.9         ( ( @'in' target ( @'module_name' @{syntax string} ) ? \<newline>
    2.10          ( @'file' @{syntax string} ) ? ( '(' args ')' ) ?) + ) ?
    2.11      ;
    2.12 @@ -2521,8 +2521,12 @@
    2.13  
    2.14    Constants may be specified by giving them literally, referring to
    2.15    all executable constants within a certain theory by giving @{text
    2.16 -  "name.*"}, or referring to \emph{all} executable constants currently
    2.17 -  available by giving @{text "*"}.
    2.18 +  "name._"}, or referring to \emph{all} executable constants currently
    2.19 +  available by giving @{text "_"}.
    2.20 +
    2.21 +  By default, exported identifiers are minimized per module.  This
    2.22 +  can be suppressed by prepending @{keyword "open"} before the list
    2.23 +  of contants.
    2.24  
    2.25    By default, for each involved theory one corresponding name space
    2.26    module is generated.  Alternatively, a module name may be specified