Re: [isabelle] Proposal: An update to Multiset theory



Dear Bertram,

> I believe multp is the more fundamental of the two predicates; after
> all, the rest of the theory is mostly concerned with the strict multiset
> extension. But I was reluctant to drop the existing multeqp predicate in
> favor of multp.

I see. I cannot find any use of "multeqp" in the repositories I mentioned in my previous email, except for some occurrences in IsaFoR. But "multeqp" can be implemented more efficiently than "multp" (and these predicates appear to be designed for code generation).

If nobody speaks up against or for one or the other predicate, I suggest you proceed with your intended change.

Cheers,

Jasmin





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