--- a/src/HOL/Library/Multiset.thy Tue Jun 11 10:30:55 2024 +0200
+++ b/src/HOL/Library/Multiset.thy Tue Jun 11 10:27:35 2024 +0200
@@ -3695,10 +3695,10 @@
by simp
lemma wfp_less_multiset[simp]:
- assumes wfp_less: "wfp ((<) :: ('a :: preorder) \<Rightarrow> 'a \<Rightarrow> bool)"
+ assumes wf: "wfp ((<) :: ('a :: preorder) \<Rightarrow> 'a \<Rightarrow> bool)"
shows "wfp ((<) :: 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool)"
unfolding less_multiset_def
- using wfp_multp[OF wfp_less] .
+ using wfp_multp[OF wf] .
subsubsection \<open>Strict total-order properties\<close>