NEWS
changeset 69733 6d158fd15b85
parent 69709 7263b59219c1
child 69743 6a9a8ef5e4c6
     1.1 --- a/NEWS	Wed Jan 23 17:54:50 2019 +0000
     1.2 +++ b/NEWS	Thu Jan 24 10:04:32 2019 +0100
     1.3 @@ -74,6 +74,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Slightly more conventional naming schema in structure Inductive.
     1.8 +Minor INCOMPATIBILITY.
     1.9 +
    1.10  * Code generation: command 'export_code' without file keyword exports
    1.11  code as regular theory export, which can be materialized using the
    1.12  command-line tool "isabelle export" or 'export_files' in the session
    1.13 @@ -139,9 +142,6 @@
    1.14  Local_Theory.open_target versus Local_Theory.close_target instead,
    1.15  or the Local_Theory.subtarget(_result) combinator. Rare INCOMPATIBILITY.
    1.16  
    1.17 -* Slightly more conventional naming schema in structure Inductive.
    1.18 -Minor INCOMPATIBILITY.
    1.19 -
    1.20  * Original PolyML.pointerEq is retained as a convenience for tools that
    1.21  don't use Isabelle/ML (where this is called "pointer_eq").
    1.22