--- a/src/HOL/Library/Multiset.thy Sun Nov 28 09:57:48 2021 +0100
+++ b/src/HOL/Library/Multiset.thy Sun Nov 28 19:12:48 2021 +0100
@@ -3193,6 +3193,12 @@
shows "M < M \<Longrightarrow> R"
by simp
+lemma wfP_less_multiset[simp]:
+ assumes wfP_less: "wfP ((<) :: ('a :: preorder) \<Rightarrow> 'a \<Rightarrow> bool)"
+ shows "wfP ((<) :: 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool)"
+ using wfP_multp[OF wfP_less] less_multiset_def
+ by (metis wfPUNIVI wfP_induct)
+
subsection \<open>Quasi-executable version of the multiset extension\<close>
--- a/src/HOL/Wellfounded.thy Sun Nov 28 09:57:48 2021 +0100
+++ b/src/HOL/Wellfounded.thy Sun Nov 28 19:12:48 2021 +0100
@@ -79,6 +79,9 @@
lemma (in wellorder) wf: "wf {(x, y). x < y}"
unfolding wf_def by (blast intro: less_induct)
+lemma (in wellorder) wfP_less[simp]: "wfP (<)"
+ by (simp add: wf wfP_def)
+
subsection \<open>Basic Results\<close>