# HG changeset patch
# User desharna
# Date 1718019886 -7200
# Node ID 31b9dfbe534c85184833a8233f4d181050dde0bb
# Parent  cdf26ac90f873f3686786055bfc6fdd06807ec09
renamed theorems

diff -r cdf26ac90f87 -r 31b9dfbe534c NEWS
--- a/NEWS	Mon Jun 10 13:39:09 2024 +0200
+++ b/NEWS	Mon Jun 10 13:44:46 2024 +0200
@@ -9,6 +9,8 @@
 
 * Theory "HOL.Wellfounded":
   - Renamed lemmas. Minor INCOMPATIBILITY.
+      accp_wfPD ~> accp_wfpD
+      accp_wfPI ~> accp_wfpI
       wfP_accp_iff ~> wfp_accp_iff
       wfP_if_convertible_to_nat ~> wfp_if_convertible_to_nat
       wfP_if_convertible_to_wfP ~> wfp_if_convertible_to_wfp
diff -r cdf26ac90f87 -r 31b9dfbe534c src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Mon Jun 10 13:39:09 2024 +0200
+++ b/src/HOL/Wellfounded.thy	Mon Jun 10 13:44:46 2024 +0200
@@ -921,7 +921,7 @@
 theorem accp_downwards: "accp r a \<Longrightarrow> r\<^sup>*\<^sup>* b a \<Longrightarrow> accp r b"
   by (blast dest: accp_downwards_aux)
 
-theorem accp_wfPI: "\<forall>x. accp r x \<Longrightarrow> wfP r"
+theorem accp_wfpI: "\<forall>x. accp r x \<Longrightarrow> wfp r"
 proof (rule wfPUNIVI)
   fix P x
   assume "\<forall>x. accp r x" "\<forall>x. (\<forall>y. r y x \<longrightarrow> P y) \<longrightarrow> P x"
@@ -929,14 +929,14 @@
     using accp_induct[where P = P] by blast
 qed
 
-theorem accp_wfPD: "wfP r \<Longrightarrow> accp r x"
+theorem accp_wfpD: "wfp r \<Longrightarrow> accp r x"
   apply (erule wfP_induct_rule)
   apply (rule accp.accI)
   apply blast
   done
 
 theorem wfp_iff_accp: "wfp r = (\<forall>x. accp r x)"
-  by (blast intro: accp_wfPI dest: accp_wfPD)
+  by (blast intro: accp_wfpI dest: accp_wfpD)
 
 
 text \<open>Smaller relations have bigger accessible parts:\<close>
@@ -986,8 +986,8 @@
 lemmas not_acc_down = not_accp_down [to_set]
 lemmas acc_downwards_aux = accp_downwards_aux [to_set]
 lemmas acc_downwards = accp_downwards [to_set]
-lemmas acc_wfI = accp_wfPI [to_set]
-lemmas acc_wfD = accp_wfPD [to_set]
+lemmas acc_wfI = accp_wfpI [to_set]
+lemmas acc_wfD = accp_wfpD [to_set]
 lemmas wf_iff_acc = wfp_iff_accp [to_set]
 lemmas acc_subset = accp_subset [to_set]
 lemmas acc_subset_induct = accp_subset_induct [to_set]