<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><br class=""><div><blockquote type="cite" class=""><div class="">On 27 Jul 2016, at 08:00, Tobias Nipkow <<a href="mailto:nipkow@in.tum.de" class="">nipkow@in.tum.de</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="">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.</div></div></blockquote><div><br class=""></div>Indeed, it will probably be tedious.</div><div><br class=""></div><div><br class=""><blockquote type="cite" class=""><div class=""><div class="">Did we ever discuss the naming issue? "insert_mset" would be the canonical name, but it would make larger expressions hard to read.<br class=""></div></div></blockquote><div><br class=""></div><div>There was some discussion in March: <a href="https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2016-March/006743.html" class="">https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2016-March/006743.html</a>, but I don't see an explicit conclusion on the best name. </div><div><br class=""></div><div>I don't remember any other discussion.</div><div><br class=""></div><div><br class=""></div><div>Mathias</div><br class=""><blockquote type="cite" class=""><div class=""><div class=""><br class="">Tobias<br class=""><br class=""><br class="">On 26/07/2016 13:59, Mathias Fleury wrote:<br class=""><blockquote type="cite" class="">Hello all,<br class=""><br class="">(Relaunching this nearly-one-and-a-half-years-old thread.)<br class=""><br class=""><br class="">Before I start working on it, has anyone already done some work towards adding insert_mset?<br class=""><br class=""><br class="">Thanks,<br class="">Mathias<br class=""><br class=""><blockquote type="cite" class="">On 08 Apr 2015, at 11:12, Larry Paulson <<a href="mailto:lp15@cam.ac.uk" class="">lp15@cam.ac.uk</a>> wrote:<br class=""><br class="">Sounds logical to me.<br class="">Larry<br class=""><br class=""><blockquote type="cite" class="">On 8 Apr 2015, at 08:13, Tobias Nipkow <<a href="mailto:nipkow@in.tum.de" class="">nipkow@in.tum.de</a>> wrote:<br class=""><br class="">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.<br class=""><br class="">Any views?<br class=""><br class="">Tobias<br class=""><br class="">_______________________________________________<br class="">isabelle-dev mailing list<br class=""><a href="mailto:isabelle-dev@in.tum.de" class="">isabelle-dev@in.tum.de</a><br class="">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev<br class=""></blockquote><br class="">_______________________________________________<br class="">isabelle-dev mailing list<br class=""><a href="mailto:isabelle-dev@in.tum.de" class="">isabelle-dev@in.tum.de</a><br class="">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev<br class=""></blockquote><br class="">_______________________________________________<br class="">isabelle-dev mailing list<br class=""><a href="mailto:isabelle-dev@in.tum.de" class="">isabelle-dev@in.tum.de</a><br class="">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev<br class=""><br class=""></blockquote><br class="">_______________________________________________<br class="">isabelle-dev mailing list<br class=""><a href="mailto:isabelle-dev@in.tum.de" class="">isabelle-dev@in.tum.de</a><br class="">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev<br class=""></div></div></blockquote></div><br class=""></body></html>