--- a/NEWS Wed Jan 23 17:54:50 2019 +0000
+++ b/NEWS Thu Jan 24 10:04:32 2019 +0100
@@ -74,6 +74,9 @@
*** HOL ***
+* Slightly more conventional naming schema in structure Inductive.
+Minor INCOMPATIBILITY.
+
* Code generation: command 'export_code' without file keyword exports
code as regular theory export, which can be materialized using the
command-line tool "isabelle export" or 'export_files' in the session
@@ -139,9 +142,6 @@
Local_Theory.open_target versus Local_Theory.close_target instead,
or the Local_Theory.subtarget(_result) combinator. Rare INCOMPATIBILITY.
-* Slightly more conventional naming schema in structure Inductive.
-Minor INCOMPATIBILITY.
-
* Original PolyML.pointerEq is retained as a convenience for tools that
don't use Isabelle/ML (where this is called "pointer_eq").