Re: [isabelle] sub-multiset relation for theory Multiset in the standard distribution


Is the subset relation defined in the obvious way for multisets? I.e. how do I write
N is a sub-multiset of M.

I know that I can define: N is a sub-multiset of M as (ALL b. count N b <= count M b) but then I will have to prove a host of properties for the sub-multiset relation.
I was wondering if the relation is already defined somewhere?



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