# HG changeset patch
# User paulson
# Date 907925231 -7200
# Node ID 5682dce0259161288cd19f1c0ddacce1757e2aa5
# Parent  707f30bc7fe756ca4555c6171ad2ebde0822543d
new theorem

diff -r 707f30bc7fe7 -r 5682dce02591 src/HOL/equalities.ML
--- 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\"";