diff -r cf86e095a439 -r 92afc125f7cd NEWS
--- a/NEWS	Thu May 29 14:18:27 2025 +0200
+++ b/NEWS	Fri May 30 07:47:03 2025 +0200
@@ -89,6 +89,9 @@
     const Set.filter
     thm filter_def → Set.filter_eq [simp]
 
+    const [List.]can_select ~> Set.can_select
+    thm can_select_def ~> Set.can_select_iff [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