diff -r 3f5382e95e1e -r d7e77cb8ce5c src/HOL/Set.ML
--- a/src/HOL/Set.ML	Thu May 30 13:31:29 1996 +0200
+++ b/src/HOL/Set.ML	Fri May 31 19:12:00 1996 +0200
@@ -319,16 +319,17 @@
 qed_goal "singletonI" Set.thy "a : {a}"
  (fn _=> [ (rtac insertI1 1) ]);
 
-qed_goal "singletonE" Set.thy "[| a: {b};  a=b ==> P |] ==> P"
- (fn major::prems=>
-  [ (rtac (major RS insertE) 1),
-    (REPEAT (eresolve_tac (prems @ [emptyE]) 1)) ]);
-
 goalw Set.thy [insert_def] "!!a. b : {a} ==> b=a";
 by (fast_tac (!claset addSEs [emptyE,CollectE,UnE]) 1);
 qed "singletonD";
 
-val singletonE = make_elim singletonD;
+bind_thm ("singletonE", make_elim singletonD);
+
+qed_goal "singleton_iff" thy "(b : {a}) = (b=a)" (fn _ => [
+	rtac iffI 1,
+	etac singletonD 1,
+	hyp_subst_tac 1,
+	rtac singletonI 1]);
 
 val [major] = goal Set.thy "{a}={b} ==> a=b";
 by (rtac (major RS equalityD1 RS subsetD RS singletonD) 1);
@@ -467,3 +468,17 @@
 
 val Pow_bottom = empty_subsetI RS PowI;        (* {}: Pow(B) *)
 val Pow_top = subset_refl RS PowI;             (* A : Pow(A) *)
+
+
+
+(*** Set reasoning tools ***)
+
+
+val mem_simps = [ Un_iff, Int_iff, Compl_iff, Diff_iff, singleton_iff,
+		  mem_Collect_eq];
+
+val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
+
+simpset := !simpset addsimps mem_simps
+                    addcongs [ball_cong,bex_cong]
+                    setmksimps (mksimps mksimps_pairs);