# HG changeset patch
# User desharna
# Date 1742133899 -3600
# Node ID 5da251ee8b58aa12dcf5c0bac43a77d424b1d1d6
# Parent  b36353e62b90eea51e2967586277352f8b973829
removed lemmas antisym_empty[simp], antisym_bot[simp], trans_empty[simp]

diff -r b36353e62b90 -r 5da251ee8b58 NEWS
--- a/NEWS	Sun Mar 16 14:51:37 2025 +0100
+++ b/NEWS	Sun Mar 16 15:04:59 2025 +0100
@@ -22,6 +22,10 @@
     the formula "r \<subset> A \<times> A \<and> refl_on A r". INCOMPATIBILITY.
   - Removed predicate single_valuedp. Use predicate right_unique instead.
     INCOMPATIBILITY.
+  - Removed lemmas. Minor INCOMPATIBILITY.
+      antisym_empty[simp] (use antisym_on_bot instead)
+      antisym_bot[simp] (use antisymp_on_bot instead)
+      trans_empty[simp] (use trans_on_bot instead)
   - Strengthened lemmas. Minor INCOMPATIBILITY.
       refl_on_empty[simp]
   - Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
diff -r b36353e62b90 -r 5da251ee8b58 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sun Mar 16 14:51:37 2025 +0100
+++ b/src/HOL/Relation.thy	Sun Mar 16 15:04:59 2025 +0100
@@ -608,14 +608,6 @@
   "r \<le> s \<Longrightarrow> antisymp s \<Longrightarrow> antisymp r"
   by (fact antisym_subset [to_pred])
     
-lemma antisym_empty [simp]:
-  "antisym {}"
-  using antisym_on_bot .
-
-lemma antisym_bot [simp]:
-  "antisymp \<bottom>"
-  using antisymp_on_bot .
-    
 lemma antisymp_on_equality[simp]: "antisymp_on A (=)"
   by (auto intro: antisymp_onI)
 
@@ -747,9 +739,6 @@
 lemma trans_on_bot[simp]: "trans_on A \<bottom>"
   by (simp add: trans_on_def)
 
-lemma trans_empty [simp]: "trans {}"
-  using trans_on_bot .
-
 lemma transp_on_bot[simp]: "transp_on A \<bottom>"
   using trans_on_bot[to_pred] .