useful lemma eqset_imp_iff
authorpaulson
Wed Dec 08 13:51:44 1999 +0100 (1999-12-08)
changeset 805337ebdaf3bb91
parent 8052 6ae3ca78a558
child 8054 2ce57ef2a4aa
useful lemma eqset_imp_iff
src/HOL/Set.ML
     1.1 --- a/src/HOL/Set.ML	Tue Dec 07 17:14:49 1999 +0100
     1.2 +++ b/src/HOL/Set.ML	Wed Dec 08 13:51:44 1999 +0100
     1.3 @@ -225,6 +225,10 @@
     1.4  by (REPEAT (resolve_tac (refl::prems) 1));
     1.5  qed "setup_induction";
     1.6  
     1.7 +Goal "A = B ==> (x : A) = (x : B)";
     1.8 +by (Asm_simp_tac 1);
     1.9 +qed "eqset_imp_iff";
    1.10 +
    1.11  
    1.12  section "The universal set -- UNIV";
    1.13