--- a/src/HOL/Finite_Set.thy Wed Aug 05 17:56:33 2020 +0100
+++ b/src/HOL/Finite_Set.thy Wed Aug 05 19:12:08 2020 +0100
@@ -1492,6 +1492,9 @@
lemma card_Un_disjoint: "finite A \<Longrightarrow> finite B \<Longrightarrow> A \<inter> B = {} \<Longrightarrow> card (A \<union> B) = card A + card B"
using card_Un_Int [of A B] by simp
+lemma card_Un_disjnt: "\<lbrakk>finite A; finite B; disjnt A B\<rbrakk> \<Longrightarrow> card (A \<union> B) = card A + card B"
+ by (simp add: card_Un_disjoint disjnt_def)
+
lemma card_Un_le: "card (A \<union> B) \<le> card A + card B"
proof (cases "finite A \<and> finite B")
case True