--- a/NEWS Mon Jun 09 22:14:38 2025 +0200
+++ b/NEWS Thu Jun 12 08:03:05 2025 +0200
@@ -104,6 +104,15 @@
const List.Bleast
discontinued in favour of more concise List.Least as variant of Min
+ const [List.]map_tailrec ~ List.map_tailrec
+ thm List.map_tailrec_eq [simp]
+
+ 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]
+
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