Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned proof
authordesharna
Fri, 21 Mar 2025 15:20:13 +0100
changeset 82314 c95eca07f6a0
parent 82313 df99e867c63e
child 82315 6c68eff8355a
tuned proof
src/HOL/Wellfounded.thy file | annotate | diff | comparison | revisions 
--- 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]
isabelle