*To*: Revantha Ramanayake <revantha at rsise.anu.edu.au>*Subject*: Re: [isabelle] sub-multiset relation for theory Multiset in the standard distribution*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Thu, 5 Jul 2007 10:24:16 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <468B45E7.7080204@rsise.anu.edu.au>*References*: <468B45E7.7080204@rsise.anu.edu.au>

Multiset.thy defines the relation mset_le as you describe.

Larry On 4 Jul 2007, at 08:01, Revantha Ramanayake wrote:

Is the subset relation defined in the obvious way for multisets?I.e. how do I writeN is a sub-multiset of M.I know that I can define: N is a sub-multiset of M as (ALL b. countN b <= count M b)but then I will have to prove a host of properties for the sub-multiset relation.I was wondering if the relation is already defined somewhere?

**Follow-Ups**:

**References**:**Re: [isabelle] sub-multiset relation for theory Multiset in the standard distribution***From:*Revantha Ramanayake

- Previous by Date: Re: [isabelle] Problem with recdef (permissive)
- Next by Date: Re: [isabelle] sub-multiset relation for theory Multiset in the standard distribution
- Previous by Thread: Re: [isabelle] sub-multiset relation for theory Multiset in the standard distribution
- Next by Thread: Re: [isabelle] sub-multiset relation for theory Multiset in the standard distribution
- Cl-isabelle-users July 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list