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