eliminate odd Unicode characters (amending e9f3b94eb6a0, b69e4da2604b, 8f0b2daa7eaa, 8d1e295aab70);
--- 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