--- a/src/HOL/Library/Multiset.thy Fri Jun 07 18:50:46 2024 +0200
+++ b/src/HOL/Library/Multiset.thy Sat Jun 08 14:57:14 2024 +0200
@@ -1548,7 +1548,7 @@
text \<open>Well-foundedness of strict subset relation\<close>
lemma wf_subset_mset_rel: "wf {(M, N :: 'a multiset). M \<subset># N}"
- using mset_subset_size wfP_def wfP_if_convertible_to_nat by blast
+ using mset_subset_size wfP_def wfp_if_convertible_to_nat by blast
lemma wfP_subset_mset[simp]: "wfP (\<subset>#)"
by (rule wf_subset_mset_rel[to_pred])