--- 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?]: