# HG changeset patch
# User haftmann
# Date 1748510148 -7200
# Node ID 0faed76929b142f475f4271f4bd1468b47bc7591
# Parent  e9f3b94eb6a0cf49f2b86029e47c4d86d9c79bab
more correct language

diff -r e9f3b94eb6a0 -r 0faed76929b1 NEWS
--- a/NEWS	Wed May 28 17:49:22 2025 +0200
+++ b/NEWS	Thu May 29 11:15:48 2025 +0200
@@ -92,8 +92,8 @@
 The _def suffix for characteristic theorems is avoided to emphasize that these
 auxiliary operations are candidates for unfolding since they are variants
 of existing logical concepts. The [simp] declarations try to move the attention
-of the casual user ways from these auxiliary operations; if they pose problems
-in existing applications, the can be removed using [simp del] – the regular
+of the casual user away from these auxiliary operations; if they expose problems
+in existing applications, they can be removed using [simp del] – the regular
 theory merge will make sure that this deviant setup will not persist in bigger
 developments. INCOMPATIBILITY.