diff -r 01c88cf514fc -r 7f240b0dabd9 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue May 02 12:51:05 2023 +0100
+++ b/src/HOL/Set.thy	Tue May 02 15:17:39 2023 +0100
@@ -1946,6 +1946,9 @@
 lemma disjnt_Un2 [simp]: "disjnt C (A \<union> B) \<longleftrightarrow> disjnt C A \<and> disjnt C B"
   by (auto simp: disjnt_def)
 
+lemma disjnt_Diff1: "disjnt (X-Y) (U-V)" and disjnt_Diff2: "disjnt (U-V) (X-Y)" if "X \<subseteq> V"
+  using that by (auto simp: disjnt_def)
+
 lemma disjoint_image_subset: "\<lbrakk>pairwise disjnt \<A>; \<And>X. X \<in> \<A> \<Longrightarrow> f X \<subseteq> X\<rbrakk> \<Longrightarrow> pairwise disjnt (f `\<A>)"
   unfolding disjnt_def pairwise_def by fast