NEWS
changeset 61859 76189756ff65
parent 61848 9250e546ab23
child 61892 5c68d06f97b3
     1.1 --- a/NEWS	Sat Dec 19 11:05:04 2015 +0100
     1.2 +++ b/NEWS	Sat Dec 19 17:03:17 2015 +0100
     1.3 @@ -346,12 +346,15 @@
     1.4      notation right.derived ("\<odot>''")
     1.5    end
     1.6  
     1.7 -* Command 'sublocale' accepts rewrite definitions after keyword
     1.8 +* Command 'global_interpreation' issues interpretations into
     1.9 +global theories, with optional rewrite definitions following keyword
    1.10  'defines'.
    1.11  
    1.12 -* Command 'permanent_interpretation' is available in Pure, without
    1.13 -need to load a separate theory.  Keyword 'defines' identifies
    1.14 -rewrite definitions, keyword 'rewrites' identifies rewrite equations.
    1.15 +* Command 'sublocale' accepts optional rewrite definitions after
    1.16 +keyword 'defines'.
    1.17 +
    1.18 +* Command 'permanent_interpretation' has been discontinued.  Use
    1.19 +'global_interpretation' or 'sublocale' instead.
    1.20  INCOMPATIBILITY.
    1.21  
    1.22  * Command 'print_definitions' prints dependencies of definitional