# HG changeset patch
# User wenzelm
# Date 1450731229 -3600
# Node ID e44d5b953f162620df1944ecd2cb7fae2bd5b533
# Parent  f5a2aed23206d232d2dc584a86616ec170d3c0c7
tuned spelling;
tuned white-space;

diff -r f5a2aed23206 -r e44d5b953f16 NEWS
--- a/NEWS	Mon Dec 21 21:50:16 2015 +0100
+++ b/NEWS	Mon Dec 21 21:53:49 2015 +0100
@@ -346,16 +346,14 @@
     notation right.derived ("\<odot>''")
   end
 
-* Command 'global_interpreation' issues interpretations into
-global theories, with optional rewrite definitions following keyword
+* Command 'global_interpretation' issues interpretations into global
+theories, with optional rewrite definitions following keyword 'defines'.
+
+* Command 'sublocale' accepts optional rewrite definitions after keyword
 'defines'.
 
-* Command 'sublocale' accepts optional rewrite definitions after
-keyword 'defines'.
-
-* Command 'permanent_interpretation' has been discontinued.  Use
-'global_interpretation' or 'sublocale' instead.
-INCOMPATIBILITY.
+* Command 'permanent_interpretation' has been discontinued. Use
+'global_interpretation' or 'sublocale' instead. INCOMPATIBILITY.
 
 * Command 'print_definitions' prints dependencies of definitional
 specifications. This functionality used to be part of 'print_theory'.