# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1616415515 0
# Node ID 76095cffcc2b25c9f3b727213656f28cda36b02e
# Parent  1e5c1f8a35cdd79425443699d2909c6d694caed6
type class relaxation

diff -r 1e5c1f8a35cd -r 76095cffcc2b src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Mar 22 00:07:55 2021 +0100
+++ b/src/HOL/Library/Multiset.thy	Mon Mar 22 12:18:35 2021 +0000
@@ -2329,7 +2329,7 @@
 
 end
 
-context ordered_cancel_comm_monoid_diff
+context cancel_comm_monoid_add
 begin
 
 lemma sum_mset_diff: