[isabelle-dev] [isabelle] Proposal: An update to Multiset theory
int-e at gmx.de
Mon Aug 8 14:44:16 CEST 2016
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 11305 bytes
Desc: not available
More information about the isabelle-dev