diff -r cccbfa567117 -r b69e4da2604b src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Fri Jun 06 18:36:29 2025 +0100 +++ b/src/HOL/Library/Multiset.thy Mon Jun 09 22:14:38 2025 +0200 @@ -4318,7 +4318,7 @@ by simp lemma [code]: "Multiset.is_empty (mset xs) \ List.null xs" - by (simp add: Multiset.is_empty_def List.null_def) + by (simp add: Multiset.is_empty_def) lemma union_code [code]: "mset xs + mset ys = mset (xs @ ys)" by simp