From ede904dc71304b8be1b989308807766c7049919e Mon Sep 17 00:00:00 2001
From: Janggun Lee <leesisi123@naver.com>
Date: Tue, 3 Sep 2024 21:27:47 +0900
Subject: [PATCH] Add changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 701574926..286da8513 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -13,6 +13,8 @@ lemma.
 * 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)
+* Add lemmas `discrete_fun_singleton_valid` and `discrete_fun_singleton_unit`, which simplify 
+  cmra validity and unit used with `discrete_fun_singleton`. (by Janggun Lee)
 
 **Changes in `proofmode`:**
 
-- 
GitLab