# HG changeset patch
# User nipkow
# Date 907259393 -7200
# Node ID 34b3366b83ac50dec77ca07f1dcee10af58325b0
# Parent  95a92bc7a5916a460a87fd90150b1d1899a62916
new singleton_conv2

diff -r 95a92bc7a591 -r 34b3366b83ac src/HOL/Set.ML
--- 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)";