src/HOL/equalities.ML

 Addsimps[Un_empty];
 
 Goal "(A Un B <= C) = (A <= C & B <= C)";
 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";
 
 Goal "A Int Compl(A) = {}";