[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 MHonArc.