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
