--- a/src/HOL/Fun_Def.thy Thu Aug 20 10:39:26 2020 +0100
+++ b/src/HOL/Fun_Def.thy Fri Aug 21 12:42:57 2020 +0100
@@ -208,7 +208,7 @@
by (auto simp: pair_less_def)
lemma total_pair_less [iff]: "total_on A pair_less" and trans_pair_less [iff]: "trans pair_less"
- by (auto simp: total_on_def pair_less_def antisym_def)
+ by (auto simp: total_on_def pair_less_def)
text \<open>Introduction rules for \<open>pair_less\<close>/\<open>pair_leq\<close>\<close>
lemma pair_leqI1: "a < b \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"