Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Wellfounded.thy
changeset 82300 838f29a19f48
parent 82299 a0693649e9c6
child 82314 c95eca07f6a0 
--- a/src/HOL/Wellfounded.thy	Mon Mar 17 16:29:48 2025 +0100
+++ b/src/HOL/Wellfounded.thy	Tue Mar 18 08:41:07 2025 +0100
@@ -530,10 +530,10 @@
 
 text \<open>Well-foundedness of the empty relation\<close>
 
-lemma wf_on_bot[simp]: "wf_on A \<bottom>"
+lemma wf_on_bot[iff]: "wf_on A \<bottom>"
   by (simp add: wf_on_def)
 
-lemma wfp_on_bot[simp]: "wfp_on A \<bottom>"
+lemma wfp_on_bot[iff]: "wfp_on A \<bottom>"
   using wf_on_bot[to_pred] .
 
 lemma wfp_empty [iff]: "wfp (\<lambda>x y. False)"
isabelle