# HG changeset patch
# User desharna
# Date 1742283667 -3600
# Node ID 838f29a19f480db9e2370be74600105447db4e86
# Parent  a0693649e9c683a5872a85fb7027bb3b5fd3591c
fixed missing from a0693649e9c6

diff -r a0693649e9c6 -r 838f29a19f48 src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Mon Mar 17 16:29:48 2025 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Tue Mar 18 08:41:07 2025 +0100
@@ -203,7 +203,7 @@
           st |>
           (PRIMITIVE (infer_instantiate ctxt [(#1 (dest_Var rel), Thm.cterm_of ctxt relation)])
             THEN (REPEAT (resolve_tac ctxt @{thms wf_mlex} 1))
-            THEN (resolve_tac ctxt @{thms wf_on_def} 1)
+            THEN (resolve_tac ctxt @{thms wf_on_bot} 1)
             THEN EVERY (map (prove_row_tac ctxt) clean_table))
         end
   end) 1 st;
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)"