--- a/NEWS Sun Mar 17 19:30:34 2024 +0100
+++ b/NEWS Sun Mar 17 19:45:07 2024 +0100
@@ -97,6 +97,8 @@
* Theory "HOL.Wellfounded":
- Added definitions wf_on and wfp_on as restricted versions versions of
wf and wfP respectively.
+ - Added wfp as alias for wfP for greater consistency with other predicates
+ such as asymp, transp, or totalp.
- Added lemmas.
wfP_iff_ex_minimal
wf_iff_ex_minimal
--- a/src/HOL/Wellfounded.thy Sun Mar 17 19:30:34 2024 +0100
+++ b/src/HOL/Wellfounded.thy Sun Mar 17 19:45:07 2024 +0100
@@ -26,6 +26,11 @@
definition wfP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
where "wfP r \<longleftrightarrow> wf {(x, y). r x y}"
+alias wfp = wfP
+
+text \<open>We keep old name \<^const>\<open>wfP\<close> for backward compatibility, but offer new name \<^const>\<open>wfp\<close> to be
+consistent with similar predicates, e.g., \<^const>\<open>asymp\<close>, \<^const>\<open>transp\<close>, \<^const>\<open>totalp\<close>.\<close>
+
subsection \<open>Equivalence of Definitions\<close>