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

[Florian Haftmann]

See now rev. 76302202a92d

Thanks for contributing!

Cheers,
	Florian

Am 08.08.2016 um 14:44 schrieb 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
> 
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160811/4e60739a/attachment.sig>