NEWS

 
 * There are some new simplification rules about multisets, the multiset
 ordering, and the subset ordering on multisets.
 INCOMPATIBILITY.
 
-* The subset ordering on multisets has now the interpretation
-ordered_ab_semigroup_monoid_add_imp_le.
+* The subset ordering on multisets has now the interpretations
+ordered_ab_semigroup_monoid_add_imp_le and bounded_lattice_bot.
 INCOMPATIBILITY.
 
 * Multiset: single has been removed in favor of add_mset that roughly
 corresponds to Set.insert. Some theorems have removed or changed:
   single_not_empty ~> add_mset_not_empty or empty_not_add_mset

   image_mset_single [simp] ~> []
   mset_subset_eq_mono_add_right_cancel [simp] ~> []
   mset_subset_eq_mono_add_left_cancel [simp] ~> []
   fold_mset_single [simp] ~> []
   subset_eq_empty [simp] ~> []
+  empty_sup [simp] ~> []
+  sup_empty [simp] ~> []
+  inter_empty [simp] ~> []
+  empty_inter [simp] ~> []
 INCOMPATIBILITY.
 
 * The order of the variables in the second cases of multiset_induct,
 multiset_induct2_size, multiset_induct2 has been changed (e.g. Add A a ~> Add a A).
 INCOMPATIBILITY.
 
 * There is now a simplification procedure on multisets. It mimics the behavior
 of the procedure on natural numbers.
+INCOMPATIBILITY.
+
+* The lemma one_step_implies_mult_aux on multisets has been removed, use
+one_step_implies_mult instead.
 INCOMPATIBILITY.
 
 * Compound constants INFIMUM and SUPREMUM are mere abbreviations now.
 INCOMPATIBILITY.