# HG changeset patch
# User lcp
# Date 788196867 -3600
# Node ID ad1d0eb0ee821cbd48864e8ec2bad60b37acaf8a
# Parent  ba386650df2c2ae66938be148f4b36c237ee8ed3
singleton_iff: new

diff -r ba386650df2c -r ad1d0eb0ee82 src/ZF/upair.ML
--- 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 ***)