diff -r a16497c686cb -r 5daa82ba4078 NEWS
--- a/NEWS	Wed Dec 09 21:20:56 2015 +0100
+++ b/NEWS	Mon Dec 07 10:49:08 2015 +0100
@@ -346,12 +346,12 @@
     notation right.derived ("\<odot>''")
   end
 
-* Command 'sublocale' accepts mixin definitions after keyword
+* Command 'sublocale' accepts rewrite definitions after keyword
 'defines'.
 
 * Command 'permanent_interpretation' is available in Pure, without
 need to load a separate theory.  Keyword 'defines' identifies
-mixin definitions, keyword 'rewrites' identifies rewrite morphisms.
+rewrite definitions, keyword 'rewrites' identifies rewrite equations.
 INCOMPATIBILITY.
 
 * Command 'print_definitions' prints dependencies of definitional