Great, thanks! Alexander
Am 06.10.2018 um 13:06 schrieb Tobias Nipkow: > Since Alexander cannot push changes, I have done so now. > > Tobias > > On 28/09/2018 18:44, Lawrence Paulson wrote: >> Sounds good to me! >> Larry >> >>> On 28 Sep 2018, at 14:00, Alexander Maletzky >>> <alexander.malet...@risc.jku.at >>> <mailto:alexander.malet...@risc.jku.at>> wrote: >>> >>> >>> lemma "sum_image_le" in theory "Groups_Big", which is stated for >>> type-class "ordered_ab_group_add", holds more generally for >>> "ordered_comm_monoid_add" (proof below). May I propose to change it >>> accordingly? >>> >>> Best regards, >>> Alexander >> >> >> >> _______________________________________________ >> 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
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev