src/HOL/Set.ML
changeset 8053 37ebdaf3bb91
parent 8025 61dde9078e24
child 8326 0e329578b0ef
     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