merged
authorpaulson
Mon, 22 Mar 2021 21:24:25 +0000
changeset 73727 41fc655585e4
parent 73726 8eeea9901897 (current diff)
parent 73723 d6209de30edc (diff)
child 73728 2cc9bd9a7357
merged
--- a/src/HOL/Library/Multiset.thy	Mon Mar 22 17:33:08 2021 +0100
+++ b/src/HOL/Library/Multiset.thy	Mon Mar 22 21:24:25 2021 +0000
@@ -2333,7 +2333,7 @@
 
 end
 
-context ordered_cancel_comm_monoid_diff
+context cancel_comm_monoid_add
 begin
 
 lemma sum_mset_diff: