Since Alexander cannot push changes, I have done so now.
Tobias On 28/09/2018 18:44, Lawrence Paulson wrote:
Sounds good to me! LarryOn 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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
