diff -r 745e518d3d0b -r 66a06a55c00c NEWS
--- a/NEWS	Sun Feb 09 22:03:07 2020 +0000
+++ b/NEWS	Mon Feb 10 21:12:52 2020 +0100
@@ -42,9 +42,9 @@
 terms: it makes a cascade of let-expressions within the derivation tree
 and may thus improve scalability.
 
-* New attribute "trace_locales" for tracing activation of locale
-instances during roundup.  It replaces the diagnostic command
-'print_dependencies', which was removed.
+* Attribute "trace_locales" activates tracing of locale instances during
+roundup. It replaces the diagnostic command 'print_dependencies', which
+has been discontinued.
 
 
 *** Isabelle/jEdit Prover IDE ***
@@ -59,10 +59,10 @@
 
 *** HOL ***
 
-* Improvements of the "lift_bnf" command:
+* Improvements of the 'lift_bnf' command:
   - Add support for quotient types.
-  - Generate transfer rules for the lifted map/set/rel/pred
-    constants (theorems "<type>.<constant>_transfer_raw").
+  - Generate transfer rules for the lifted map/set/rel/pred constants
+    (theorems "<type>.<constant>_transfer_raw").
 
 * Term_XML.Encode/Decode.term uses compact representation of Const
 "typargs" from the given declaration environment. This also makes more
@@ -71,13 +71,13 @@
 applications.
 
 * ASCII membership syntax concerning big operators for infimum and
-supremum is gone. INCOMPATIBILITY.
+supremum has been discontinued. INCOMPATIBILITY.
 
 * Clear distinction between types for bits (False / True) and Z2 (0 /
-1): theory HOL/Library/Bit.thy has been renamed accordingly.
-INCOMPATIBILITY.
-
-* Fact collections algebra_split_simps and field_split_simps correspond
+1): theory HOL-Library.Bit has been renamed accordingly.
+INCOMPATIBILITY.
+
+* Dynamic facts "algebra_split_simps" and "field_split_simps" correspond
 to algebra_simps and field_simps but contain more aggressive rules
 potentially splitting goals; algebra_split_simps roughly replaces
 sign_simps and field_split_simps can be used instead of divide_simps.
@@ -95,7 +95,7 @@
 * Session HOL-Analysis: proof method "metric" implements a decision
 procedure for simple linear statements in metric spaces.
 
-* Word: Bitwise NOT-operator has proper prefix syntax.  Minor
+* Session HOL-Word: Bitwise NOT-operator has proper prefix syntax. Minor
 INCOMPATIBILITY.