src/ZF/upair.ML
changeset 12372 cd3a09c7dac9
parent 11589 9a6d4511bb3c
equal deleted inserted replaced
12371:80ca9058db95 12372:cd3a09c7dac9
    82 by (blast_tac (claset() addSIs prems) 1);
    82 by (blast_tac (claset() addSIs prems) 1);
    83 qed "UnCI";
    83 qed "UnCI";
    84 
    84 
    85 AddSIs [UnCI];
    85 AddSIs [UnCI];
    86 AddSEs [UnE];
    86 AddSEs [UnE];
    87 AddXEs [UnI1, UnI2];
       
    88 
    87 
    89 
    88 
    90 (*** Rules for small intersection -- Int -- defined via Upair ***)
    89 (*** Rules for small intersection -- Int -- defined via Upair ***)
    91 
    90 
    92 Goalw [Int_def]  "c : A Int B <-> (c:A & c:B)";
    91 Goalw [Int_def]  "c : A Int B <-> (c:A & c:B)";