--- a/NEWS Sun Jun 09 22:40:13 2024 +0200
+++ b/NEWS Mon Jun 10 08:25:55 2024 +0200
@@ -9,8 +9,10 @@
* Theory "HOL.Wellfounded":
- Renamed lemmas. Minor INCOMPATIBILITY.
+ 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
+ wf_acc_iff ~> wf_iff_acc
New in Isabelle2024 (May 2024)
--- a/src/HOL/List.thy Sun Jun 09 22:40:13 2024 +0200
+++ b/src/HOL/List.thy Mon Jun 10 08:25:55 2024 +0200
@@ -7383,7 +7383,7 @@
qed
lemma wf_listrel1_iff[simp]: "wf(listrel1 r) = wf r"
-by (auto simp: wf_acc_iff
+by (auto simp: wf_iff_acc
intro: lists_accD lists_accI[THEN Cons_in_lists_iff[THEN iffD1, THEN conjunct1]])
subsubsection \<open>Lifting Relations to Lists: all elements\<close>
--- a/src/HOL/Wellfounded.thy Sun Jun 09 22:40:13 2024 +0200
+++ b/src/HOL/Wellfounded.thy Mon Jun 10 08:25:55 2024 +0200
@@ -935,7 +935,7 @@
apply blast
done
-theorem wfP_accp_iff: "wfP r = (\<forall>x. accp r x)"
+theorem wfp_iff_accp: "wfp r = (\<forall>x. accp r x)"
by (blast intro: accp_wfPI dest: accp_wfPD)
@@ -988,7 +988,7 @@
lemmas acc_downwards = accp_downwards [to_set]
lemmas acc_wfI = accp_wfPI [to_set]
lemmas acc_wfD = accp_wfPD [to_set]
-lemmas wf_acc_iff = wfP_accp_iff [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]