singleton_iff: new

--- a/src/ZF/upair.ML	Fri Dec 23 16:33:37 1994 +0100
+++ b/src/ZF/upair.ML	Fri Dec 23 16:34:27 1994 +0100
@@ -166,6 +166,9 @@
   [ (rtac (major RS consE) 1),
     (REPEAT (eresolve_tac (prems @ [emptyE]) 1)) ]);
 
+qed_goal "singleton_iff" ZF.thy "a : {b} <-> a=b"
+ (fn _ => [ (fast_tac (lemmas_cs addIs [consI1] addSEs [consE]) 1) ]);
+
 
 (*** Rules for Descriptions ***)