# HG changeset patch
# User nipkow
# Date 870421168 -7200
# Node ID b87c86b6c29157c8e15f3202c80f410be1e68fc0
# Parent  0727ebd62b48513250de1a4bef5183115476145f
Added {x.x=a} = a to !simpset.

diff -r 0727ebd62b48 -r b87c86b6c291 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Fri Jul 25 14:31:48 1997 +0200
+++ b/src/HOL/Set.ML	Fri Aug 01 09:39:28 1997 +0200
@@ -415,6 +415,10 @@
     
 AddSDs [singleton_inject];
 
+goal Set.thy "{x.x=a} = {a}";
+by(Blast_tac 1);
+qed "singleton_conv";
+Addsimps [singleton_conv];
 
 section "The universal set -- UNIV";