# HG changeset patch
# User desharna
# Date 1654357738 -7200
# Node ID 4e3e55aedd7f37151bdad64ed72b39b98b5318b2
# Parent  6bd264ff410f973340a15d0f4912bb560ba6aec7
replaced HOL.implies by Pure.imp in reflp_mono for consistency with other lemmas

diff -r 6bd264ff410f -r 4e3e55aedd7f NEWS
--- a/NEWS	Sat Jun 04 17:42:04 2022 +0200
+++ b/NEWS	Sat Jun 04 17:48:58 2022 +0200
@@ -45,6 +45,8 @@
     Lemma reflp_def is explicitly provided for backward compatibility
     but its usage is discouraged. Minor INCOMPATIBILITY.
   - Added predicate totalp_on and abbreviation totalp.
+  - Replaced HOL.implies by Pure.imp in lemma reflp_mono for consistency
+    with other lemmas. Minor INCOMPATIBILITY.
   - Added lemmas.
       preorder.asymp_greater
       preorder.asymp_less
diff -r 6bd264ff410f -r 4e3e55aedd7f src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sat Jun 04 17:42:04 2022 +0200
+++ b/src/HOL/Relation.thy	Sat Jun 04 17:48:58 2022 +0200
@@ -244,7 +244,7 @@
   "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"
   by (auto intro: reflp_onI dest: reflp_onD)
 
-lemma reflp_mono: "reflp R \<Longrightarrow> (\<And>x y. R x y \<longrightarrow> Q x y) \<Longrightarrow> reflp Q"
+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