new singleton_conv2

--- a/src/HOL/Set.ML	Thu Oct 01 18:29:38 1998 +0200
+++ b/src/HOL/Set.ML	Thu Oct 01 18:29:53 1998 +0200
@@ -460,6 +460,11 @@
 qed "singleton_conv";
 Addsimps [singleton_conv];
 
+Goal "{x. a=x} = {a}";
+by(Blast_tac 1);
+qed "singleton_conv2";
+Addsimps [singleton_conv2];
+
 
 section "Unions of families -- UNION x:A. B(x) is Union(B``A)";