diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4b290acc607ea8deeb1d72795438d25b6cd30c72..522940facb4d79ced8ee5dec57aa2a8ecac95ed5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -105,6 +105,10 @@ Coq 8.13 is no longer supported.
 * Add `âˆ—-âˆ—` as notation in `stdpp_scope` similar to `-âˆ—`. This means `P âˆ—-âˆ— Q`
   can be directly used as lemma statement, and is syntactic sugar for `âŠ¢ P âˆ—-âˆ— Q`.
 * Add `â‰¼` connective (`internal_included`) on the BI level. (by Ike Mulder)
+* Move laws of persistence modality out of `BiMixin` into `BiPersistentlyMixin`.
+* Provide smart constructor `bi_persistently_mixin_discrete` for
+  `BiPersistentlyMixin`: Given a discrete BI that enjoys the existential
+  property, a trivial definition of the persistence modality can be given.
 
 **Changes in `proofmode`:**