--- 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";