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,