308 mset_remdups_le ~> mset_remdups_subset_eq |
308 mset_remdups_le ~> mset_remdups_subset_eq |
309 ms_lesseq_impl ~> subset_eq_mset_impl |
309 ms_lesseq_impl ~> subset_eq_mset_impl |
310 |
310 |
311 Some functions have been renamed: |
311 Some functions have been renamed: |
312 ms_lesseq_impl -> subset_eq_mset_impl |
312 ms_lesseq_impl -> subset_eq_mset_impl |
|
313 |
|
314 * Multisets are now ordered with the multiset ordering |
|
315 #\<subseteq># ~> \<le> |
|
316 #\<subset># ~> < |
|
317 le_multiset ~> less_eq_multiset |
|
318 less_multiset ~> le_multiset |
|
319 INCOMPATIBILITY |
|
320 |
|
321 * The prefix multiset_order has been discontinued: the theorems can be directly |
|
322 accessed. |
|
323 INCOMPATILBITY |
|
324 |
|
325 * Some theorems about the multiset ordering have been renamed: |
|
326 le_multiset_def ~> less_eq_multiset_def |
|
327 less_multiset_def ~> le_multiset_def |
|
328 less_eq_imp_le_multiset ~> subset_eq_imp_le_multiset |
|
329 mult_less_not_refl ~> mset_le_not_refl |
|
330 mult_less_trans ~> mset_le_trans |
|
331 mult_less_not_sym ~> mset_le_not_sym |
|
332 mult_less_asym ~> mset_le_asym |
|
333 mult_less_irrefl ~> mset_le_irrefl |
|
334 union_less_mono2{,1,2} ~> union_le_mono2{,1,2} |
|
335 |
|
336 le_multiset\<^sub>H\<^sub>O ~> less_eq_multiset\<^sub>H\<^sub>O |
|
337 le_multiset_total ~> less_eq_multiset_total |
|
338 less_multiset_right_total ~> subset_eq_imp_le_multiset |
|
339 le_multiset_empty_left ~> less_eq_multiset_empty_left |
|
340 le_multiset_empty_right ~> less_eq_multiset_empty_right |
|
341 less_multiset_empty_right ~> le_multiset_empty_left |
|
342 less_multiset_empty_left ~> le_multiset_empty_right |
|
343 union_less_diff_plus ~> union_le_diff_plus |
|
344 ex_gt_count_imp_less_multiset ~> ex_gt_count_imp_le_multiset |
|
345 less_multiset_plus_left_nonempty ~> le_multiset_plus_left_nonempty |
|
346 le_multiset_plus_right_nonempty ~> le_multiset_plus_right_nonempty |
|
347 less_multiset_plus_plus_left_iff ~> le_multiset_plus_plus_left_iff |
|
348 less_multiset_plus_plus_right_iff ~> le_multiset_plus_plus_right_iff |
|
349 INCOMPATIBILITY |
313 |
350 |
314 * Compound constants INFIMUM and SUPREMUM are mere abbreviations now. |
351 * Compound constants INFIMUM and SUPREMUM are mere abbreviations now. |
315 INCOMPATIBILITY. |
352 INCOMPATIBILITY. |
316 |
353 |
317 * More complex analysis including Cauchy's inequality, Liouville theorem, |
354 * More complex analysis including Cauchy's inequality, Liouville theorem, |