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