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