> On 27 Jul 2016, at 08:00, Tobias Nipkow <nip...@in.tum.de> wrote: > > No, we keep talking about it (internally), but nobody at TUM has done > anything about it. It would be great if you want to take this on. It is > potentially tedious because there are many existing uses of multisets.
Indeed, it will probably be tedious. > Did we ever discuss the naming issue? "insert_mset" would be the canonical > name, but it would make larger expressions hard to read. There was some discussion in March: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2016-March/006743.html <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2016-March/006743.html>, but I don't see an explicit conclusion on the best name. I don't remember any other discussion. Mathias > > Tobias > > > On 26/07/2016 13:59, Mathias Fleury wrote: >> Hello all, >> >> (Relaunching this nearly-one-and-a-half-years-old thread.) >> >> >> Before I start working on it, has anyone already done some work towards >> adding insert_mset? >> >> >> Thanks, >> Mathias >> >>> On 08 Apr 2015, at 11:12, Larry Paulson <l...@cam.ac.uk> wrote: >>> >>> Sounds logical to me. >>> Larry >>> >>>> On 8 Apr 2015, at 08:13, Tobias Nipkow <nip...@in.tum.de> wrote: >>>> >>>> Currently the setup in Multiset is geared towards having the 3 basic >>>> (non-free) constructors: empty, singleton and union. Although induction >>>> already has only two cases (empty and union with singleton), it would be >>>> nicer to have only two constructors, like for finite sets: empty and >>>> insert. In particular, this often avoids the use of ac_simps for union >>>> because representations are more canonical. The singleton constructor >>>> would be retained as an abbreviation for "insert_mset _ {#}" but "M + >>>> {#x#}" would be simplified to "insert_mset x M", like for sets. >>>> >>>> Any views? >>>> >>>> Tobias >>>> >>>> _______________________________________________ >>>> isabelle-dev mailing list >>>> isabelle-...@in.tum.de >>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >>> >>> _______________________________________________ >>> isabelle-dev mailing list >>> isabelle-...@in.tum.de >>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >> >> _______________________________________________ >> isabelle-dev mailing list >> isabelle-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >> > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
