--- a/NEWS Sun Jan 22 23:29:34 2023 +0100
+++ b/NEWS Mon Jan 23 13:31:07 2023 +0100
@@ -66,6 +66,8 @@
be abbreviations. Lemmas trans_def and transp_def are explicitly provided
for backward compatibility but their usage is discouraged.
Minor INCOMPATIBILITY.
+ - Renamed wrongly named lemma totalp_on_refl_on_eq to totalp_on_total_on_eq.
+ Minor INCOMPATIBILITY.
- Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
antisym_converse[simp] ~> antisym_on_converse[simp]
order.antisymp_ge[simp] ~> order.antisymp_on_ge[simp]
--- a/src/HOL/Relation.thy Sun Jan 22 23:29:34 2023 +0100
+++ b/src/HOL/Relation.thy Mon Jan 23 13:31:07 2023 +0100
@@ -751,7 +751,7 @@
abbreviation totalp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
"totalp \<equiv> totalp_on UNIV"
-lemma totalp_on_refl_on_eq[pred_set_conv]: "totalp_on A (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> total_on A r"
+lemma totalp_on_total_on_eq[pred_set_conv]: "totalp_on A (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> total_on A r"
by (simp add: totalp_on_def total_on_def)
lemma total_onI [intro?]: