From b83e6cad26f4525db23f10d330a3b1a941689dae Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 17 Nov 2022 16:43:06 +0100
Subject: [PATCH] CHANGELOG.

---
 CHANGELOG.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6dd343903..54670738d 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`:**
 
-- 
GitLab