moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
as there have been unnecessary proofs of anonymous thms, which could not be
removed (by name) from the !simpset where necessary. All these thms except
singleton_iff were already proved in Set.ML.
therefore in Set.ML: New version of singletonE, proof of new thm singleton_iff

--- a/src/HOL/Fun.ML	Thu May 30 13:31:29 1996 +0200
+++ b/src/HOL/Fun.ML	Fri May 31 19:12:00 1996 +0200
@@ -190,20 +190,3 @@
             subsetD, subsetCE];
 
 fun cfast_tac prems = cut_facts_tac prems THEN' fast_tac set_cs;
-
-
-fun prover s = prove_goal Fun.thy s (fn _=>[fast_tac set_cs 1]);
-
-val mem_simps = map prover
- [ "(a : A Un B)   =  (a:A | a:B)",	(* Un_iff *)
-   "(a : A Int B)  =  (a:A & a:B)",	(* Int_iff *)
-   "(a : Compl(B)) =  (~a:B)",		(* Compl_iff *)
-   "(a : A-B)      =  (a:A & ~a:B)",	(* Diff_iff *)
-   "(a : {b})      =  (a=b)",
-   "(a : {x.P(x)}) =  P(a)" ];
-
-val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
-
-simpset := !simpset addsimps mem_simps
-                    addcongs [ball_cong,bex_cong]
-                    setmksimps (mksimps mksimps_pairs);

--- 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);