--- 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;--- 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)"