From 844c94bab187bbaf09da496d22d036885d989cae Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Thu, 7 Feb 2019 20:52:51 +0100
Subject: Add the eqType instance for intervals, le_bound(l|r)_anti, and
 itv_intersection, redefine prev_of_itv and itv_decompose using lersif, extend
 itv_rewrite, simplify proofs (#271)

---
 ChangeLog | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'ChangeLog')

diff --git a/ChangeLog b/ChangeLog
index 49a850a..81d479a 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -14,7 +14,10 @@
 
 	* Extended theory about homo and mono for leq/or and Num.le
 
-	* Extended theory of lersif and intervals
+	* Changed and extended theory of lersif and intervals:
+	  * Many lersif related lemmas are ported from ssrnum
+	  * Definitions that changed: prev_of_itv, itv_decompose, and itv_rewrite
+	  * Theory of intersections of intervals is added
 
 	* Renamed: (together with the _in suffix counterpart)
 	  mono_inj -> incr_inj
-- 
cgit v1.2.3