Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Weak lemma: sum_mset_diff

Email Gateway (Mar 21 2021 at 22:25):

From: Jakub Kądziołka <kuba@kadziolka.net>
Hello,

HOL-Library.Multiset.sum_mset_diff is proven for the ordered_cancel_comm_monoid_diff
type class. However, the more general cancel_comm_monoid_add is
sufficient.

Regards,
Jakub Kądziołka

Email Gateway (Jul 15 2022 at 15:46):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
For the record: this has been generalized by Larry in Rev. 76095cffcc2b

Cheers,
Florian
OpenPGP_signature

Last updated: Jan 04 2025 at 20:18 UTC