--- 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.