--- a/src/HOL/equalities.ML Tue Aug 18 10:24:54 1998 +0200
+++ b/src/HOL/equalities.ML Tue Aug 18 10:25:13 1998 +0200
@@ -331,6 +331,10 @@
by (Blast_tac 1);
qed "Un_subset_iff";
+Goal "(A - B) Un (A Int B) = A";
+by (Blast_tac 1);
+qed "Un_Diff_Int";
+
section "Compl";