# HG changeset patch
# User wenzelm
# Date 1753107697 -7200
# Node ID 45107da819fc4e53a3c69c215c44a1ef3105491f
# Parent  372273ab6ebbc8b72f74cf141442af6d3afc2bf0
eliminate odd Unicode characters (amending e9f3b94eb6a0, b69e4da2604b, 8f0b2daa7eaa, 8d1e295aab70);

diff -r 372273ab6ebb -r 45107da819fc NEWS
--- a/NEWS	Mon Jul 21 15:10:00 2025 +0200
+++ b/NEWS	Mon Jul 21 16:21:37 2025 +0200
@@ -127,17 +127,17 @@
     const List.Bleast
     discontinued in favour of more concise Lattices_Big.Least
 
-    const [List.]map_tailrec ~ List.map_tailrec
+    const [List.]map_tailrec ~> List.map_tailrec
     thm List.map_tailrec_eq [simp]
 
-    const [List.]gen_length → List.length_tailrec
+    const [List.]gen_length ~> List.length_tailrec
     thm List.length_tailrec_eq [simp]
 
-    const [List.]maps → List.maps
-    thm maps_def → List.maps_eq [simp]
-
-    const [List.]map_project → Option.image_filter
-    thm map_project_def → Option.image_filter_eq
+    const [List.]maps ~> List.maps
+    thm maps_def ~> List.maps_eq [simp]
+
+    const [List.]map_project ~> Option.image_filter
+    thm map_project_def ~> Option.image_filter_eq
 
 The _def suffix for characteristic theorems is avoided to emphasize that these
 auxiliary operations are candidates for unfolding since they are variants