From 9f5a604dacd0fd335559b573f93b04bf6033d1cd Mon Sep 17 00:00:00 2001 From: Olivier Laurent Date: Tue, 12 May 2020 09:03:20 +0200 Subject: fuse changelogs for #11249 and #12237 --- doc/changelog/10-standard-library/11249-ollibs-list-changelog.rst | 7 ++++--- doc/changelog/10-standard-library/12237-list-more-filter-incl.rst | 4 ---- 2 files changed, 4 insertions(+), 7 deletions(-) delete mode 100644 doc/changelog/10-standard-library/12237-list-more-filter-incl.rst (limited to 'doc') diff --git a/doc/changelog/10-standard-library/11249-ollibs-list-changelog.rst b/doc/changelog/10-standard-library/11249-ollibs-list-changelog.rst index be15fbf8f5..be54e45808 100644 --- a/doc/changelog/10-standard-library/11249-ollibs-list-changelog.rst +++ b/doc/changelog/10-standard-library/11249-ollibs-list-changelog.rst @@ -7,11 +7,12 @@ - properties of ``remove``: ``remove_cons``, ``remove_app``, ``notin_remove``, ``in_remove``, ``in_in_remove``, ``remove_remove_comm``, ``remove_remove_eq``, ``remove_length_le``, ``remove_length_lt`` - properties of ``concat``: ``in_concat``, ``remove_concat`` - properties of ``map`` and ``flat_map``: ``map_last``, ``map_eq_cons``, ``map_eq_app``, ``flat_map_app``, ``flat_map_ext``, ``nth_nth_nth_map`` - - properties of ``incl``: ``incl_nil_l``, ``incl_l_nil``, ``incl_cons_inv``, ``incl_app_app``, ``incl_app_inv``, ``remove_incl`` + - properties of ``incl``: ``incl_nil_l``, ``incl_l_nil``, ``incl_cons_inv``, ``incl_app_app``, ``incl_app_inv``, ``remove_incl``, ``incl_map``, ``incl_filter``, ``incl_Forall_in_iff`` + - properties of ``NoDup`` and ``nodup``: ``NoDup_rev``, ``NoDup_filter``, ``nodup_incl`` - properties of ``Exists`` and ``Forall``: ``Exists_nth``, ``Exists_app``, ``Exists_rev``, ``Exists_fold_right``, ``incl_Exists``, ``Forall_nth``, ``Forall_app``, ``Forall_elt``, ``Forall_rev``, ``Forall_fold_right``, ``incl_Forall``, ``map_ext_Forall``, ``Exists_or``, ``Exists_or_inv``, ``Forall_and``, ``Forall_and_inv``, ``exists_Forall``, ``Forall_image``, ``concat_nil_Forall``, ``in_flat_map_Exists``, ``notin_flat_map_Forall`` - properties of ``repeat``: ``repeat_cons``, ``repeat_to_concat`` - definitions and properties of ``list_sum`` and ``list_max``: ``list_sum_app``, ``list_max_app``, ``list_max_le``, ``list_max_lt`` - - misc: ``elt_eq_unit``, ``last_length``, ``rev_eq_app``, ``removelast_firstn_len``, ``NoDup_rev``, ``nodup_incl``, ``cons_seq``, ``seq_S`` + - misc: ``elt_eq_unit``, ``last_length``, ``rev_eq_app``, ``removelast_firstn_len``, ``cons_seq``, ``seq_S`` - (`#11249 `_, + (`#11249 `_, `#12237 `_, by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/12237-list-more-filter-incl.rst b/doc/changelog/10-standard-library/12237-list-more-filter-incl.rst deleted file mode 100644 index 37aaf697b5..0000000000 --- a/doc/changelog/10-standard-library/12237-list-more-filter-incl.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - new lemmas in ``List``: ``incl_map``, ``incl_filter``, ``NoDup_filter``, ``incl_Forall_in_iff`` - (`#12237 `_, - by Olivier Laurent). -- cgit v1.2.3