# HG changeset patch
# User desharna
# Date 1742566813 -3600
# Node ID c95eca07f6a09b96d51eb8e5a7cb4939b602bf71
# Parent  df99e867c63e39e131874b0941e6a1b8a2e22d9a
tuned proof

diff -r df99e867c63e -r c95eca07f6a0 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Fri Mar 21 14:21:44 2025 +0100
+++ b/src/HOL/Wellfounded.thy	Fri Mar 21 15:20:13 2025 +0100
@@ -524,7 +524,7 @@
 text \<open>Well-foundedness of subsets\<close>
 
 lemma wf_subset: "wf r \<Longrightarrow> p \<subseteq> r \<Longrightarrow> wf p"
-  by (simp add: wf_eq_minimal) fast
+  using wf_on_antimono[OF subset_UNIV, unfolded le_bool_def] ..
 
 lemmas wfp_subset = wf_subset [to_pred]