new thm and simprule Compl_Diff_eq

--- a/src/HOL/equalities.ML	Mon Aug 14 18:49:35 2000 +0200
+++ b/src/HOL/equalities.ML	Wed Aug 16 10:22:41 2000 +0200
@@ -795,6 +795,11 @@
 qed "Diff_Compl";
 Addsimps [Diff_Compl];
 
+Goal "- (A-B) = -A Un B";
+by (blast_tac (claset() addIs []) 1); 
+qed "Compl_Diff_eq";
+Addsimps [Compl_Diff_eq];
+
 
 section "Quantification over type \"bool\"";