| changeset 61518 | ff12606337e9 |
| parent 61378 | 3e04c9ca001a |
| child 61799 | 4cf66f21b764 |
--- 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