Re: [isabelle-dev] Lemma "sum_image_le"

2018-10-06 Thread Alexander Maletzky
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 >>> >>

Re: [isabelle-dev] Lemma "sum_image_le"

2018-10-06 Thread 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 > wrote: lemma "sum_image_le" in theory "Groups_Big", which is stated

Re: [isabelle-dev] Lemma "sum_image_le"

2018-09-28 Thread Lawrence Paulson
Sounds good to me! Larry > On 28 Sep 2018, at 14:00, Alexander Maletzky > 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 >

[isabelle-dev] Lemma "sum_image_le"

2018-09-28 Thread Alexander Maletzky
Dear list, 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 lemma sum_image_le:   fixes g :: "'a ⇒