[isabelle-dev] Multiset insert

[Tobias Nipkow]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5059 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20150408/88ca3b60/attachment-0001.p7s>