# HG changeset patch
# User desharna
# Date 1711615258 -3600
# Node ID 804a41d08b8420baa9ee90a8e5b5b189120143a6
# Parent  c40bdfc846408c2a44ba6163e886656ca95f36ab
tuned proof

diff -r c40bdfc84640 -r 804a41d08b84 src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Wed Mar 27 18:29:32 2024 +0100
+++ b/src/HOL/Library/Multiset_Order.thy	Thu Mar 28 09:40:58 2024 +0100
@@ -813,7 +813,16 @@
 lemma wf_less_multiset: "wf {(M :: 'a multiset, N). M < N}"
   unfolding less_multiset_def multp_def by (auto intro: wf_mult wf)
 
-instance by standard (metis less_multiset_def multp_def wf wf_def wf_mult)
+instance
+proof intro_classes
+  fix P :: "'a multiset \<Rightarrow> bool" and a :: "'a multiset"
+  have "wfp ((<) :: 'a \<Rightarrow> 'a \<Rightarrow> bool)"
+    using wfp_on_less .
+  hence "wfp ((<) :: 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool)"
+    unfolding less_multiset_def by (rule wfP_multp)
+  thus "(\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P a"
+    unfolding wfp_on_def[of UNIV, simplified] by metis
+qed
 
 end