NEWS
changeset 82669 92afc125f7cd
parent 82665 0faed76929b1
child 82674 f4441890dee0
child 82677 c603d41dc183
--- 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