NEWS
changeset 61895 e44d5b953f16
parent 61892 5c68d06f97b3
child 61907 f0c894ab18c9
     1.1 --- a/NEWS	Mon Dec 21 21:50:16 2015 +0100
     1.2 +++ b/NEWS	Mon Dec 21 21:53:49 2015 +0100
     1.3 @@ -346,16 +346,14 @@
     1.4      notation right.derived ("\<odot>''")
     1.5    end
     1.6  
     1.7 -* Command 'global_interpreation' issues interpretations into
     1.8 -global theories, with optional rewrite definitions following keyword
     1.9 +* Command 'global_interpretation' issues interpretations into global
    1.10 +theories, with optional rewrite definitions following keyword 'defines'.
    1.11 +
    1.12 +* Command 'sublocale' accepts optional rewrite definitions after keyword
    1.13  'defines'.
    1.14  
    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 +* Command 'permanent_interpretation' has been discontinued. Use
    1.22 +'global_interpretation' or 'sublocale' instead. INCOMPATIBILITY.
    1.23  
    1.24  * Command 'print_definitions' prints dependencies of definitional
    1.25  specifications. This functionality used to be part of 'print_theory'.