--- a/NEWS Wed Feb 26 10:10:38 2014 +0100
+++ b/NEWS Wed Feb 26 11:57:52 2014 +0100
@@ -91,9 +91,14 @@
*** HOL ***
+* Code generator: explicit proof contexts in many ML interfaces.
+INCOMPATIBILITY.
+
* Code generator: minimize exported identifiers by default.
+Minor INCOMPATIBILITY.
* Code generation for SML and OCaml: dropped arcane "no_signatures" option.
+Minor INCOMPATIBILITY.
* Simproc "finite_Collect" is no longer enabled by default, due to
spurious crashes and other surprises. Potential INCOMPATIBILITY.