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
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 ⇒
Some notions defined in "Frag.thy" already exist in "Poly_Mapping.thy":
"support" is called "keys" there, and I think "frag_cmul" could easily
be defined in terms of "map".
"frag_extend" looks like a special case of a more general subsitution
homomorphism "subst" of type "('a => 'b => 'c) => ('a
