diff -r 5e3aa998e94e -r d08128985789 equalities.ML
--- a/equalities.ML	Wed Dec 22 12:43:37 1993 +0100
+++ b/equalities.ML	Thu Dec 30 10:19:44 1993 +0100
@@ -10,6 +10,16 @@
 
 val eq_cs = set_cs addSIs [equalityI];
 
+(** : **)
+
+goal Set.thy "x ~: {}";
+by(fast_tac set_cs 1);
+val in_empty = result();
+
+goal Set.thy "x : insert(y,A) = (x=y | x:A)";
+by(fast_tac set_cs 1);
+val in_insert = result();
+
 (** insert **)
 
 goal Set.thy "!!a. a:A ==> insert(a,A) = A";
@@ -263,7 +273,8 @@
 val Diff_Int = result();
 
 val set_ss = set_ss addsimps
-  [Int_absorb,Int_empty_left,Int_empty_right,
+  [in_empty,in_insert,
+   Int_absorb,Int_empty_left,Int_empty_right,
    Un_absorb,Un_empty_left,Un_empty_right,
    constant_UN,image_empty,
    Compl_disjoint,double_complement,