diff options
| author | Kazuhiko Sakaguchi | 2019-02-07 20:52:51 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2019-02-07 20:52:51 +0100 |
| commit | 844c94bab187bbaf09da496d22d036885d989cae (patch) | |
| tree | 2f479912f128dfd21aae8d8923f481491a19c725 /ChangeLog | |
| parent | 5ba21e9d4a2ec934f09dc316603df83eee345d41 (diff) | |
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)
Diffstat (limited to 'ChangeLog')
| -rw-r--r-- | ChangeLog | 5 |
1 files changed, 4 insertions, 1 deletions
@@ -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 |