--- 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
--- 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>