--- a/src/HOL/Relation.thy Mon Mar 24 14:04:11 2025 +0100
+++ b/src/HOL/Relation.thy Mon Mar 24 14:05:55 2025 +0100
@@ -264,9 +264,6 @@
lemma reflp_on_mono[mono]: "A \<subseteq> B \<Longrightarrow> R \<le> Q \<Longrightarrow> reflp_on B R \<le> reflp_on A Q"
by (simp add: reflp_on_mono_strong le_fun_def)
-lemma reflp_mono: "reflp R \<Longrightarrow> (\<And>x y. R x y \<Longrightarrow> Q x y) \<Longrightarrow> reflp Q"
- using reflp_on_mono_strong[OF _ subset_UNIV] .
-
lemma (in preorder) reflp_on_le[simp]: "reflp_on A (\<le>)"
by (simp add: reflp_onI)