[isabelle] converting a multiset to a list
Hi, this question concerns multisets as defined in the theory file
Multisets in the standard distribution.
It is easy to define the function multiset_of :: " 'a list => 'a
multiset " which forms a multiset from a list in the obvious way.
How do I define a function (of type " 'a multiset => 'a list ") that
accepts a multiset and returns a list (where each
occurrence in the multiset is an occurrence in the list and vice versa)
? I realize
that there are many possible output lists. I am interested in obtaining
one such list.
This archive was generated by a fusion of
Pipermail (Mailman edition) and