[isabelle-dev] [isabelle] Proposal: An update to Multiset theory

[Bertram Felgenhauer]

Florian Haftmann wrote:
> Hi Bertram,
> 
> > How shall we proceed? As I hinted at earlier I do not have (nor want, at
> > this point) push access, but I can prepare a patch or clone of the repo,
> > if that helps, or just provide a plain theory file that works with the
> > development version of Isabelle.
> 
> a repo URL or a patch is indeed the best thing to proceed: there is not
> »the« development version but an ongoing agile development.

Okay, I have exported a series of two patches against 1e7c5bbea36d,
the first adding monotonicity lemmata and the second for cancellation
and `multp`, `multeq`. See the attached file.

Cheers,

Bertram
-------------- next part --------------
A non-text attachment was scrubbed...
Name: multiset.patch
Type: text/x-diff
Size: 11305 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160808/b49dc5de/attachment-0001.patch>