--- 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,