# HG changeset patch
# User paulson
# Date 1616415523 0
# Node ID d6209de30edcf86d074d3414b5d0b526f26e280d
# Parent  ee1c4962671cd236648a64eff7be90856b6531f7# Parent  76095cffcc2b25c9f3b727213656f28cda36b02e
merged

diff -r ee1c4962671c -r d6209de30edc src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Mar 22 10:49:51 2021 +0000
+++ b/src/HOL/Library/Multiset.thy	Mon Mar 22 12:18:43 2021 +0000
@@ -2333,7 +2333,7 @@
 
 end
 
-context ordered_cancel_comm_monoid_diff
+context cancel_comm_monoid_add
 begin
 
 lemma sum_mset_diff: