# HG changeset patch
# User desharna
# Date 1710701107 -3600
# Node ID 8d153846f65fa2793d47e7ac0ec6e43eb8fa7089
# Parent  6fc9c4344df428fe69c172e2889cf7459feded58
added alias wfp for wfP

diff -r 6fc9c4344df4 -r 8d153846f65f NEWS
--- 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
diff -r 6fc9c4344df4 -r 8d153846f65f src/HOL/Wellfounded.thy
--- 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>