Re: [isabelle] Multiset elements

Hi Christian,

Am 22.08.2014 um 14:58 schrieb Christian Sternagel <c.sternagel at>:

> there's also a "copy" of Multiset (called Multiset_Extension) in the AFP entry Well-Quasi-Orders. The point here was to have the multiset extension of an arbitrary order (given as predicate of type "'a => 'a => bool") over a fixed carrier set (not a full type).
> This theory is not polished at all, but maybe it contains something useful. At some point I'll have to clean this up ...

We did need a multiset extension of the multiset order itself, so Dmitriy had to develop similar stuff in our private "Multiset_More" theory. We need to look more closely into this, but a priori we are interested.



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