--- a/src/HOL/Fun_Def.thy Sun Aug 16 11:57:15 2020 +0200
+++ b/src/HOL/Fun_Def.thy Mon Aug 17 15:42:38 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)
+ by (auto simp: total_on_def pair_less_def antisym_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"