--- a/src/HOL/Wellfounded.thy Fri Jun 07 18:50:46 2024 +0200
+++ b/src/HOL/Wellfounded.thy Sat Jun 08 14:57:14 2024 +0200
@@ -1065,16 +1065,16 @@
using convertible .
qed
-lemma wfP_if_convertible_to_wfP: "wfP S \<Longrightarrow> (\<And>x y. R x y \<Longrightarrow> S (f x) (f y)) \<Longrightarrow> wfP R"
+lemma wfp_if_convertible_to_wfp: "wfP S \<Longrightarrow> (\<And>x y. R x y \<Longrightarrow> S (f x) (f y)) \<Longrightarrow> wfP R"
using wf_if_convertible_to_wf[to_pred, of S R f] by simp
text \<open>Converting to @{typ nat} is a very common special case that might be found more easily by
Sledgehammer.\<close>
-lemma wfP_if_convertible_to_nat:
+lemma wfp_if_convertible_to_nat:
fixes f :: "_ \<Rightarrow> nat"
shows "(\<And>x y. R x y \<Longrightarrow> f x < f y) \<Longrightarrow> wfP R"
- by (rule wfP_if_convertible_to_wfP[of "(<) :: nat \<Rightarrow> nat \<Rightarrow> bool", simplified])
+ by (rule wfp_if_convertible_to_wfp[of "(<) :: nat \<Rightarrow> nat \<Rightarrow> bool", simplified])
subsubsection \<open>Measure functions into \<^typ>\<open>nat\<close>\<close>