From 197d868c8b097f83df418182529b86dda07cbcd9 Mon Sep 17 00:00:00 2001
From: Janggun Lee <leesisi123@naver.com>
Date: Thu, 29 Aug 2024 11:44:54 +0900
Subject: [PATCH] Add changelog.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5fab43e31..701574926 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -10,6 +10,9 @@ lemma.
 * Add lemmas `big_opS_gset_to_gmap` and `big_opS_gset_to_gmap_L`, which rewrite
   between `gset_to_gmap` and big set ops of singleton maps.  (by Isaac van
   Bakel)
+* Add lemmas `discrete_fun_update` and `discrete_fun_updateP`, which updates an
+  abitrary `discrete_fun` to another. For `discrete_fun_updateP`, this requires
+  the domain to be finite, similar to `discrete_fun_included_spec`. (by Janggun Lee)
 
 **Changes in `proofmode`:**
 
-- 
GitLab