diff -r c64628dbac00 -r ff12606337e9 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Set.thy	Mon Oct 26 23:41:27 2015 +0000
@@ -1552,6 +1552,9 @@
 lemma Diff_Int: "A - (B \<inter> C) = (A - B) \<union> (A - C)"
   by blast
 
+lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B"
+  by blast
+
 lemma Un_Diff: "(A \<union> B) - C = (A - C) \<union> (B - C)"
   by blast