# HG changeset patch
# User paulson
# Date 952104173 -3600
# Node ID 226d12ac76e2e6af3cde26ca06544e337d2b0c08
# Parent  88fe0f1a480f4ac33543e26b0a6cd5253340448d
improved reasoning about {} and UNIV

diff -r 88fe0f1a480f -r 226d12ac76e2 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Fri Mar 03 02:00:43 2000 +0100
+++ b/src/HOL/equalities.ML	Fri Mar 03 18:22:53 2000 +0100
@@ -374,10 +374,14 @@
 
 section "Set complement";
 
-Goal "A Int (-A) = {}";
+Goal "A Int -A = {}";
 by (Blast_tac 1);
 qed "Compl_disjoint";
-Addsimps[Compl_disjoint];
+
+Goal "-A Int A = {}";
+by (Blast_tac 1);
+qed "Compl_disjoint2";
+Addsimps[Compl_disjoint, Compl_disjoint2];
 
 Goal "A Un (-A) = UNIV";
 by (Blast_tac 1);
@@ -415,6 +419,16 @@
 by (blast_tac (claset() addSEs [equalityCE]) 1);
 qed "Un_Int_assoc_eq";
 
+Goal "-UNIV = {}";
+by (Blast_tac 1);
+qed "Compl_UNIV_eq";
+
+Goal "-{} = UNIV";
+by (Blast_tac 1);
+qed "Compl_empty_eq";
+
+Addsimps [Compl_UNIV_eq, Compl_empty_eq];
+
 
 section "Union";