diff -r a0693649e9c6 -r 838f29a19f48 src/HOL/Wellfounded.thy
--- 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)"