NEWS
changeset 55757 9fc71814b8c1
parent 55716 2a6a8f9d52e1
child 55818 d8b2f50705d0
     1.1 --- a/NEWS	Wed Feb 26 10:10:38 2014 +0100
     1.2 +++ b/NEWS	Wed Feb 26 11:57:52 2014 +0100
     1.3 @@ -91,9 +91,14 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Code generator: explicit proof contexts in many ML interfaces.
     1.8 +INCOMPATIBILITY.
     1.9 +
    1.10  * Code generator: minimize exported identifiers by default.
    1.11 +Minor INCOMPATIBILITY.
    1.12  
    1.13  * Code generation for SML and OCaml: dropped arcane "no_signatures" option.
    1.14 +Minor INCOMPATIBILITY.
    1.15  
    1.16  * Simproc "finite_Collect" is no longer enabled by default, due to
    1.17  spurious crashes and other surprises.  Potential INCOMPATIBILITY.