new theorem

--- a/src/HOL/equalities.ML	Fri Oct 09 11:25:26 1998 +0200
+++ b/src/HOL/equalities.ML	Fri Oct 09 11:27:11 1998 +0200
@@ -706,6 +706,11 @@
 by (Blast_tac 1);
 qed "Diff_Int_distrib2";
 
+Goal "A - - B = A Int B";
+by Auto_tac;
+qed "Diff_Compl";
+Addsimps [Diff_Compl];
+
 
 section "Quantification over type \"bool\"";