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
