NEWS
changeset 69829 3bfa28b3a5b2
parent 69828 74d673b7d40e
child 69854 cc0b3e177b49
     1.1 --- a/NEWS	Thu Feb 21 09:15:06 2019 +0000
     1.2 +++ b/NEWS	Thu Feb 21 09:15:07 2019 +0000
     1.3 @@ -104,6 +104,10 @@
     1.4  * Slightly more conventional naming schema in structure Inductive.
     1.5  Minor INCOMPATIBILITY.
     1.6  
     1.7 +* Various _global variants of specification tools have been removed.
     1.8 +Minor INCOMPATIBILITY, prefer combinators Named_Target.theory_map[_result]
     1.9 +to lift specifications to the global theory level.
    1.10 +
    1.11  * Code generation: command 'export_code' without file keyword exports
    1.12  code as regular theory export, which can be materialized using the
    1.13  command-line tools "isabelle export" or "isabelle build -e" (with