equal
deleted
inserted
replaced
31 sup_subset_mset ~> union_mset |
31 sup_subset_mset ~> union_mset |
32 multiset_inter_def ~> inter_mset_def |
32 multiset_inter_def ~> inter_mset_def |
33 sup_subset_mset_def ~> union_mset_def |
33 sup_subset_mset_def ~> union_mset_def |
34 multiset_inter_count ~> count_inter_mset |
34 multiset_inter_count ~> count_inter_mset |
35 sup_subset_mset_count ~> count_union_mset |
35 sup_subset_mset_count ~> count_union_mset |
|
36 |
|
37 * Theory Multiset: syntax precendence for membership operations has been |
|
38 adjusted to match the corresponding precendences on sets. Rare |
|
39 INCOMPATIBILITY. |
36 |
40 |
37 * HOL-Analysis/HOL-Probability: indexed products of discrete |
41 * HOL-Analysis/HOL-Probability: indexed products of discrete |
38 distributions, negative binomial distribution, Hoeffding's inequality, |
42 distributions, negative binomial distribution, Hoeffding's inequality, |
39 Chernoff bounds, Cauchy–Schwarz inequality for nn_integral, and some |
43 Chernoff bounds, Cauchy–Schwarz inequality for nn_integral, and some |
40 more small lemmas. Some theorems that were stated awkwardly before were |
44 more small lemmas. Some theorems that were stated awkwardly before were |