# HG changeset patch
# User desharna
# Date 1674477067 -3600
# Node ID 1c358879bfd319d0998e62896b2ff7fad82d5a96
# Parent  39f8051f71d422ce197b009f0996043f6805a255
proper name for lemma totalp_on_total_on_eq

diff -r 39f8051f71d4 -r 1c358879bfd3 NEWS
--- 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]
diff -r 39f8051f71d4 -r 1c358879bfd3 src/HOL/Relation.thy
--- 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?]: