1.1 --- a/src/HOL/equalities.ML	Tue Aug 18 10:24:54 1998 +0200
     1.2 +++ b/src/HOL/equalities.ML	Tue Aug 18 10:25:13 1998 +0200
     1.3 @@ -331,6 +331,10 @@
     1.4  by (Blast_tac 1);
     1.5  qed "Un_subset_iff";
     1.6  
     1.7 +Goal "(A - B) Un (A Int B) = A";
     1.8 +by (Blast_tac 1);
     1.9 +qed "Un_Diff_Int";
    1.10 +
    1.11  
    1.12  section "Compl";
    1.13