From 449ced9b0cca36544cab074b8d4f7465e870ad3a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 19 Jul 2022 11:05:03 -0400
Subject: [PATCH] changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index c9c805bb5..8a6d6efdb 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -33,6 +33,10 @@ lemma.
   second a universal, so let's use the appropriate notation. Also use double
   quantifiers (`∀∀`, `∃∃`) to make it clear that these are not normal
   quantifiers (the latter change was also applied to logically atomic triples).
+* Add some lemmas to show properties of functions defined via monotonoe fixpoints:
+  `least_fixpoint_affine`, `least_fixpoint_absorbing`,
+  `least_fixpoint_persistent_affine`, `least_fixpoint_persistent_absorbing`,
+  `greatest_fixpoint_absorbing`.
 
 **Changes in `proofmode`:**
 
-- 
GitLab