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
I was wondering if the relation is already defined somewhere?
This archive was generated by a fusion of
Pipermail (Mailman edition) and