Re: [isabelle] Mapping multisets



Peter,

On Tue, 2008-09-30 at 16:03 +0100, Peter Chapman wrote:
> How can I define a map for multisets, similar to the one for lists

theory Multiset in Isabelle 2008 already contains

  "image_mset f == fold_mset (op + o single o f) {#}"

See http://isabelle.in.tum.de/dist/library/HOL/Library/Multiset.html for
further details.

Best,
Tjark






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