# HG changeset patch
# User desharna
# Date 1665675082 -7200
# Node ID a00c80314b06cbb0d73e5be95f7225c3e1a4833c
# Parent  8e777e0e206a83212e8ff6caea48947f54f49950
strengthened lemmas preorder.reflp_ge[simp] and preorder.reflp_le[simp]

diff -r 8e777e0e206a -r a00c80314b06 NEWS
--- a/NEWS	Thu Oct 13 17:22:34 2022 +0200
+++ b/NEWS	Thu Oct 13 17:31:22 2022 +0200
@@ -14,7 +14,10 @@
     Minor INCOMPATIBILITY.
 
 * Theory "HOL.Relation":
-  - Strengthened lemma total_on_singleton. Minor INCOMPATIBILITY.
+  - Strengthened lemmas. Minor INCOMPATIBILITY.
+      preorder.reflp_ge
+      preorder.reflp_le
+      total_on_singleton
   - Added lemmas.
       antisym_if_asymp
       antisymp_if_asymp
diff -r 8e777e0e206a -r a00c80314b06 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Thu Oct 13 17:22:34 2022 +0200
+++ b/src/HOL/Relation.thy	Thu Oct 13 17:31:22 2022 +0200
@@ -256,11 +256,11 @@
 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 (\<le>)"
-  by (simp add: reflpI)
+lemma (in preorder) reflp_le[simp]: "reflp_on A (\<le>)"
+  by (simp add: reflp_onI)
 
-lemma (in preorder) reflp_ge[simp]: "reflp (\<ge>)"
-  by (simp add: reflpI)
+lemma (in preorder) reflp_ge[simp]: "reflp_on A (\<ge>)"
+  by (simp add: reflp_onI)
 
 
 subsubsection \<open>Irreflexivity\<close>