# HG changeset patch
# User paulson
# Date 966414161 -7200
# Node ID a50dcf0475ad9b3ffc7f51104aeb80ad682dd49a
# Parent  449b6108352a47d5b2e303af2f6fab039b151042
new thm and simprule Compl_Diff_eq

diff -r 449b6108352a -r a50dcf0475ad src/HOL/equalities.ML
--- 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\"";