# HG changeset patch
# User desharna
# Date 1742821555 -3600
# Node ID 81c920587d49fad2527d6f6ab2240d72a119cffe
# Parent  575f8f5c8e311b0e8758632e797d2ad5a73bdf21
removed reflp_mono (use reflp_on_mono_strong instead)

diff -r 575f8f5c8e31 -r 81c920587d49 NEWS
--- a/NEWS	Mon Mar 24 14:04:11 2025 +0100
+++ b/NEWS	Mon Mar 24 14:05:55 2025 +0100
@@ -47,8 +47,9 @@
   - Removed predicate single_valuedp. Use predicate right_unique instead.
     INCOMPATIBILITY.
   - Removed lemmas. Minor INCOMPATIBILITY.
+      antisym_bot[simp] (use antisymp_on_bot instead)
       antisym_empty[simp] (use antisym_on_bot instead)
-      antisym_bot[simp] (use antisymp_on_bot instead)
+      reflp_mono (use reflp_on_mono_strong instead)
       trans_empty[simp] (use trans_on_bot instead)
   - Strengthened lemmas. Minor INCOMPATIBILITY.
       refl_on_empty[simp]
diff -r 575f8f5c8e31 -r 81c920587d49 src/HOL/Relation.thy
--- 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)