--- a/src/HOL/List.thy Wed May 21 20:44:12 2025 +0200
+++ b/src/HOL/List.thy Thu May 22 19:59:43 2025 +0200
@@ -3769,6 +3769,9 @@
case False with d show ?thesis by auto
qed
+lemma distinct_concat_rev[simp]: "distinct (concat (rev xs)) = distinct (concat xs)"
+by (induction xs) auto
+
lemma distinct_concat:
"\<lbrakk> distinct xs;
\<And> ys. ys \<in> set xs \<Longrightarrow> distinct ys;
@@ -4285,6 +4288,7 @@
qed
qed
+
subsection \<open>@{const distinct_adj}\<close>
lemma distinct_adj_Nil [simp]: "distinct_adj []"