# HG changeset patch
# User paulson
# Date 944657504 -3600
# Node ID 37ebdaf3bb91bc3d7e5f2c98e1150ac97e894863
# Parent  6ae3ca78a5582a6a18afc309d8b4966a4f27b33f
useful lemma eqset_imp_iff

diff -r 6ae3ca78a558 -r 37ebdaf3bb91 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Tue Dec 07 17:14:49 1999 +0100
+++ b/src/HOL/Set.ML	Wed Dec 08 13:51:44 1999 +0100
@@ -225,6 +225,10 @@
 by (REPEAT (resolve_tac (refl::prems) 1));
 qed "setup_induction";
 
+Goal "A = B ==> (x : A) = (x : B)";
+by (Asm_simp_tac 1);
+qed "eqset_imp_iff";
+
 
 section "The universal set -- UNIV";