author | lcp |
Fri, 23 Dec 1994 16:34:27 +0100 | |
changeset 834 | ad1d0eb0ee82 |
parent 833 | ba386650df2c |
child 835 | 313ac9b513f1 |
src/ZF/upair.ML | file | annotate | diff | comparison | revisions |
--- 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 ***)