# HG changeset patch
# User desharna
# Date 1669193879 -3600
# Node ID 608489919ecf4b61c1004ea1a1d9234c99dbec4b
# Parent  df6ba3cf7874da470692e84d40f8fb7dd5d10d09
strengthened and renamed irreflp_greater[simp] and irreflp_less[simp]

diff -r df6ba3cf7874 -r 608489919ecf NEWS
--- a/NEWS	Wed Nov 23 09:54:53 2022 +0100
+++ b/NEWS	Wed Nov 23 09:57:59 2022 +0100
@@ -31,8 +31,10 @@
     explicitly provided for backward compatibility but their usage is
     discouraged. Minor INCOMPATIBILITY.
   - Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
+      preorder.irreflp_greater[simp] ~> irreflp_on_greater[simp]
+      preorder.irreflp_less[simp] ~> irreflp_on_less[simp]
+      reflp_equality[simp] ~> reflp_on_equality[simp]
       total_on_singleton
-      reflp_equality[simp] ~> reflp_on_equality[simp]
   - Added lemmas.
       antisym_if_asymp
       antisymp_if_asymp
diff -r df6ba3cf7874 -r 608489919ecf src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Nov 23 09:54:53 2022 +0100
+++ b/src/HOL/Library/Multiset.thy	Wed Nov 23 09:57:59 2022 +0100
@@ -3433,7 +3433,7 @@
   fix M N :: "'a multiset"
   show "(M < N) = (M \<le> N \<and> \<not> N \<le> M)"
     unfolding less_eq_multiset_def less_multiset_def
-    by (metis irreflp_def irreflp_less irreflp_multp transpE transp_less transp_multp)
+    by (metis irreflp_def irreflp_on_less irreflp_multp transpE transp_less transp_multp)
 next
   fix M :: "'a multiset"
   show "M \<le> M"
@@ -3450,7 +3450,7 @@
   show "M \<le> N \<Longrightarrow> N \<le> M \<Longrightarrow> M = N"
     unfolding less_eq_multiset_def less_multiset_def
     using transp_multp[OF transp_less, THEN transpD]
-    using irreflp_multp[OF transp_less irreflp_less, unfolded irreflp_def, rule_format]
+    using irreflp_multp[OF transp_less irreflp_on_less, unfolded irreflp_def, rule_format]
     by blast
 qed
 
diff -r df6ba3cf7874 -r 608489919ecf src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Wed Nov 23 09:54:53 2022 +0100
+++ b/src/HOL/Relation.thy	Wed Nov 23 09:57:59 2022 +0100
@@ -326,11 +326,11 @@
 lemma irreflp_on_subset: "irreflp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> irreflp_on B R"
   by (auto simp: irreflp_on_def)
 
-lemma (in preorder) irreflp_less[simp]: "irreflp (<)"
-  by (simp add: irreflpI)
+lemma (in preorder) irreflp_on_less[simp]: "irreflp_on A (<)"
+  by (simp add: irreflp_onI)
 
-lemma (in preorder) irreflp_greater[simp]: "irreflp (>)"
-  by (simp add: irreflpI)
+lemma (in preorder) irreflp_on_greater[simp]: "irreflp_on A (>)"
+  by (simp add: irreflp_onI)
 
 subsubsection \<open>Asymmetry\<close>