On 13/02/2021 10:51, Florian Haftmann wrote:
Hi all, after the current Isabelle release I want to take up some notes for things which can still be polished in the multiset theory. I want to excite feedback especially from those who spent a lot of work there in recent times (as far as I remember, Jasmin, beside others). 1. Names not following the *_mset convention * Melem → member_mset * Mempty → empty_mset
2. Names of definitions deviating for historic reasons * inf_subset_mset → inter_mset * sup_subset_mset → union_mset
3. Names for the multiset ordering Names mult1 and mult, in a larger setting, are ambiguous. Possible ideas: * mult1 → multiset_order_step | Multiset.order_step * mult → multiset_order_rel | Multiset.order_rel But alternative names must be really convincing to justify such a transition.
I chose the current names and they are clearly bad. Now I would go for multiset_order and multiset_order_step. But Jasmin and friends may have a more informed opinion because of their work on extended multiset orders.
Description: S/MIME Cryptographic Signature