Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Weak lemma: sum_mset_diff


view this post on Zulip 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


Last updated: Dec 05 2021 at 23:19 UTC