diff -r 21c405b4039f -r ccbbe1264c0f equalities.ML
--- a/equalities.ML	Sun Jan 29 14:02:17 1995 +0100
+++ b/equalities.ML	Mon Jan 30 16:32:32 1995 +0100
@@ -62,7 +62,7 @@
 by (fast_tac eq_cs 1);
 qed "Int_empty_right";
 
-goal Set.thy "(A Un B) Int C  =  (A Int C) Un (B Int C)";
+goal Set.thy "A Int (B Un C)  =  (A Int B) Un (A Int C)";
 by (fast_tac eq_cs 1);
 qed "Int_Un_distrib";
 
@@ -113,6 +113,10 @@
 by (fast_tac eq_cs 1);
 qed "subset_insert_iff";
 
+goal Set.thy "(A Un B = {}) = (A = {} & B = {})";
+by (fast_tac (eq_cs addEs [equalityCE]) 1);
+qed "Un_empty";
+
 (** Simple properties of Compl -- complement of a set **)
 
 goal Set.thy "A Int Compl(A) = {}";
@@ -322,7 +326,7 @@
 val set_ss = set_ss addsimps
   [in_empty,in_insert,insert_subset,
    Int_absorb,Int_empty_left,Int_empty_right,
-   Un_absorb,Un_empty_left,Un_empty_right,
+   Un_absorb,Un_empty_left,Un_empty_right,Un_empty,
    UN1_constant,image_empty,
    Compl_disjoint,double_complement,
    Union_empty,Union_insert,empty_subsetI,subset_refl,