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