[isabelle] Some more polishing of the multiset theory



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.

Cheers,
	Florian

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.