# HG changeset patch
# User wenzelm
# Date 1728077884 -7200
# Node ID 7b3b27576f45cbc3ac7e0d8bc1fd5fb4e9febdde
# Parent  6538332c08e0694775198ffb2a46e6b6178cf4b1
misc tuning;

diff -r 6538332c08e0 -r 7b3b27576f45 NEWS
--- a/NEWS	Fri Oct 04 15:21:01 2024 +0200
+++ b/NEWS	Fri Oct 04 23:38:04 2024 +0200
@@ -36,16 +36,16 @@
 *** Isabelle/VSCode Prover IDE ***
 
 * General improvements: Persistent decorations for PIDE markup, correct
-  font and formatting in panels, and proper completions.
-  Moreover, the PIDE extension of the LSP now features additional
-  protocol messages (e.g. to obtain the set of Isabelle symbols) and
-  more fine-grained control for unicode symbols.
-
-* Active "sendback" markup can now be used via LSP code actions, e.g.
-  to insert proof methods from Sledgehammer output.
+font and formatting in panels, and proper completions. Moreover, the
+PIDE extension of the LSP now features additional protocol messages
+(e.g. to obtain the set of Isabelle symbols) and more fine-grained
+control for recoding of Unicode symbols.
+
+* Active "sendback" markup can now be used via LSP code actions, e.g. to
+insert proof methods from Sledgehammer output.
 
 * Relevant Isabelle options can now be overriden from the
-  Isabelle/VSCode extension settings.
+Isabelle/VSCode extension settings.
 
 
 *** HOL ***
@@ -65,7 +65,7 @@
 
 * Theory "HOL.Wellfounded":
   - Removed lemma wellorder.wfP_less. Use wellorder.wfp_on_less instead.
-    Minor INCOMPATIBILITIES.
+    Minor INCOMPATIBILITY.
   - Renamed lemmas. Minor INCOMPATIBILITY.
       accp_wfPD ~> accp_wfpD
       accp_wfPI ~> accp_wfpI
@@ -99,13 +99,13 @@
       image_mset_diff_if_inj
       minus_add_mset_if_not_in_lhs[simp]
 
-* Transitioinal theory "Divides" moved to "HOL-Library.Divides" and supposed to
-be removed in a furure release.  Minor INCOMPATIBILITY.  Import
-"HOL-Library.Divides" and keep an eye on theorems prefixed with "Divides." to
-ease transition.
+* Transitioinal theory "Divides" moved to "HOL-Library.Divides" and
+supposed to be removed in a furure release. Minor INCOMPATIBILITY.
+Import "HOL-Library.Divides" and keep an eye on theorems prefixed with
+"Divides." to ease transition.
 
 * The real-valued versions of ln, log, powr have been totalised by
-ln(0) = x and ln(-x) = ln(x). Many related theorems are now
+"ln(0) = x" and "ln(-x) = ln(x)". Many related theorems are now
 unconditional, with ln_mult_pos and ln_divide_pos introduced for legacy
 purposes.