diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6dd3439030f094624e4174c86d85b2e958a84927..54670738d570f38ba1cec56fc93ec6f4d7d1e900 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -9,6 +9,8 @@ lemma.
 
 * Add a construction `bi_tc` to create transitive closures of
   PROP-level binary relations.
+* Use `binder` in notations for big ops. This means one can write things such
+  as `[∗ map] '(k,_) ↦ '(_,y) ∈ m, ⌜ k = y ⌝`.
 
 **Changes in `proofmode`:**