# HG changeset patch
# User desharna
# Date 1718094455 -7200
# Node ID 7d4cd57cd955d632d3a6034b2e1f2d04ed307885
# Parent  f05a71fa1a3f7661e5d524f9ae4d4a02c9bce3ef
tuned proof

diff -r f05a71fa1a3f -r 7d4cd57cd955 src/HOL/Library/Multiset.thy
--- 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>