clarifying NEWS file
authorfleury <Mathias.Fleury@mpi-inf.mpg.de>
Sat Oct 08 13:50:25 2016 +0200 (2016-10-08)
changeset 64097331fbf2a0d2d
parent 64096 5edeb60a7ec5
child 64112 84c1ae86b9af
clarifying NEWS file
NEWS
     1.1 --- a/NEWS	Fri Oct 07 23:11:20 2016 +0200
     1.2 +++ b/NEWS	Sat Oct 08 13:50:25 2016 +0200
     1.3 @@ -529,9 +529,6 @@
     1.4      mset_lessD ~> mset_subsetD
     1.5      mset_le_insertD ~> mset_subset_eq_insertD
     1.6      mset_less_of_empty ~> mset_subset_of_empty
     1.7 -    le_empty ~> subset_eq_empty
     1.8 -    mset_less_add_bothsides ~> mset_subset_add_bothsides
     1.9 -    mset_less_empty_nonempty ~> mset_subset_empty_nonempty
    1.10      mset_less_size ~> mset_subset_size
    1.11      wf_less_mset_rel ~> wf_subset_mset_rel
    1.12      count_le_replicate_mset_le ~> count_le_replicate_mset_subset_eq
    1.13 @@ -578,8 +575,6 @@
    1.14      ex_gt_count_imp_less_multiset ~> ex_gt_count_imp_le_multiset
    1.15      less_multiset_plus_left_nonempty ~> le_multiset_plus_left_nonempty
    1.16      le_multiset_plus_right_nonempty ~> le_multiset_plus_right_nonempty
    1.17 -    less_multiset_plus_plus_left_iff ~> le_multiset_plus_plus_left_iff
    1.18 -    less_multiset_plus_plus_right_iff ~> le_multiset_plus_plus_right_iff
    1.19  INCOMPATIBILITY.
    1.20  
    1.21  * HOL-Library: the lemma mset_map has now the attribute [simp].
    1.22 @@ -589,16 +584,22 @@
    1.23  INCOMPATIBILITY, use the following replacements:
    1.24  
    1.25      le_multiset_plus_plus_left_iff ~> add_less_cancel_right
    1.26 +    less_multiset_plus_plus_left_iff ~> add_less_cancel_right
    1.27      le_multiset_plus_plus_right_iff ~> add_less_cancel_left
    1.28 +    less_multiset_plus_plus_right_iff ~> add_less_cancel_left
    1.29      add_eq_self_empty_iff ~> add_cancel_left_right
    1.30      mset_subset_add_bothsides ~> subset_mset.add_less_cancel_right
    1.31 +    mset_less_add_bothsides ~> subset_mset.add_less_cancel_right
    1.32 +    mset_le_add_bothsides ~> subset_mset.add_less_cancel_right
    1.33      empty_inter ~> subset_mset.inf_bot_left
    1.34      inter_empty ~> subset_mset.inf_bot_right
    1.35      empty_sup ~> subset_mset.sup_bot_left
    1.36      sup_empty ~> subset_mset.sup_bot_right
    1.37      bdd_below_multiset ~> subset_mset.bdd_above_bot
    1.38      subset_eq_empty ~> subset_mset.le_zero_eq
    1.39 +    le_empty ~> subset_mset.le_zero_eq
    1.40      mset_subset_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero
    1.41 +    mset_less_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero
    1.42  
    1.43  * HOL-Library: some typeclass constraints about multisets have been
    1.44  reduced from ordered or linordered to preorder. Multisets have the