# HG changeset patch
# User desharna
# Date 1669051412 -3600
# Node ID 41c92fcb8805d6284e514670d8d9bcf1c4a4a41b
# Parent  4d6d8dfd2cd2ffbded3742f5aba9cc5ddc24b529# Parent  3fc92362fbb51862a60ac13b1b7259675b7e25a6
merged

diff -r 4d6d8dfd2cd2 -r 41c92fcb8805 NEWS
--- a/NEWS	Mon Nov 21 16:21:49 2022 +0000
+++ b/NEWS	Mon Nov 21 18:23:32 2022 +0100
@@ -26,25 +26,24 @@
     Minor INCOMPATIBILITY.
 
 * Theory "HOL.Relation":
-  - Strengthened lemmas. Minor INCOMPATIBILITY.
-      preorder.reflp_ge
-      preorder.reflp_le
+  - Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
       total_on_singleton
+      reflp_equality[simp] ~> reflp_on_equality[simp]
   - Added lemmas.
       antisym_if_asymp
       antisymp_if_asymp
       irreflD
       irreflpD
-      linorder.totalp_ge[simp]
-      linorder.totalp_greater[simp]
-      linorder.totalp_le[simp]
-      linorder.totalp_less[simp]
+      linorder.totalp_on_ge[simp]
+      linorder.totalp_on_greater[simp]
+      linorder.totalp_on_le[simp]
+      linorder.totalp_on_less[simp]
       order.antisymp_ge[simp]
       order.antisymp_le[simp]
       preorder.antisymp_greater[simp]
       preorder.antisymp_less[simp]
-      preorder.reflp_ge[simp]
-      preorder.reflp_le[simp]
+      preorder.reflp_on_ge[simp]
+      preorder.reflp_on_le[simp]
       reflp_on_conversp[simp]
       totalp_on_singleton[simp]
 
diff -r 4d6d8dfd2cd2 -r 41c92fcb8805 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Nov 21 16:21:49 2022 +0000
+++ b/src/HOL/Relation.thy	Mon Nov 21 18:23:32 2022 +0100
@@ -246,8 +246,8 @@
   "refl_on A r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<in> A \<and> y \<in> A) \<and> (\<forall>x \<in> A. (x, x) \<in> r)"
   by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
 
-lemma reflp_equality [simp]: "reflp (=)"
-  by (simp add: reflp_def)
+lemma reflp_on_equality [simp]: "reflp_on A (=)"
+  by (simp add: reflp_on_def)
 
 lemma reflp_on_mono:
   "reflp_on A R \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> Q x y) \<Longrightarrow> reflp_on A Q"
@@ -256,10 +256,10 @@
 lemma reflp_mono: "reflp R \<Longrightarrow> (\<And>x y. R x y \<Longrightarrow> Q x y) \<Longrightarrow> reflp Q"
   by (rule reflp_on_mono[of UNIV R Q]) simp_all
 
-lemma (in preorder) reflp_le[simp]: "reflp_on A (\<le>)"
+lemma (in preorder) reflp_on_le[simp]: "reflp_on A (\<le>)"
   by (simp add: reflp_onI)
 
-lemma (in preorder) reflp_ge[simp]: "reflp_on A (\<ge>)"
+lemma (in preorder) reflp_on_ge[simp]: "reflp_on A (\<ge>)"
   by (simp add: reflp_onI)
 
 
@@ -593,16 +593,16 @@
 lemma totalp_on_singleton [simp]: "totalp_on {x} R"
   by (simp add: totalp_on_def)
 
-lemma (in linorder) totalp_less[simp]: "totalp_on A (<)"
+lemma (in linorder) totalp_on_less[simp]: "totalp_on A (<)"
   by (auto intro: totalp_onI)
 
-lemma (in linorder) totalp_greater[simp]: "totalp_on A (>)"
+lemma (in linorder) totalp_on_greater[simp]: "totalp_on A (>)"
   by (auto intro: totalp_onI)
 
-lemma (in linorder) totalp_le[simp]: "totalp_on A (\<le>)"
+lemma (in linorder) totalp_on_le[simp]: "totalp_on A (\<le>)"
   by (rule totalp_onI, rule linear)
 
-lemma (in linorder) totalp_ge[simp]: "totalp_on A (\<ge>)"
+lemma (in linorder) totalp_on_ge[simp]: "totalp_on A (\<ge>)"
   by (rule totalp_onI, rule linear)