src/ZF/ex/CoUnit.ML
changeset 527 35c70ab82940
parent 515 abcc438e7c27
child 760 f0200e91b272
equal deleted inserted replaced
526:85d7ff169b9c 527:35c70ab82940
    56 by (etac trans_induct 1);
    56 by (etac trans_induct 1);
    57 by (safe_tac subset_cs);
    57 by (safe_tac subset_cs);
    58 by (etac counit2.elim 1);
    58 by (etac counit2.elim 1);
    59 by (etac counit2.elim 1);
    59 by (etac counit2.elim 1);
    60 by (rewrite_goals_tac counit2.con_defs);
    60 by (rewrite_goals_tac counit2.con_defs);
       
    61 val lleq_cs = subset_cs
       
    62 	addSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono]
       
    63         addSEs [Ord_in_Ord, Pair_inject];
    61 by (fast_tac lleq_cs 1);
    64 by (fast_tac lleq_cs 1);
    62 val counit2_Int_Vset_subset_lemma = result();
    65 val counit2_Int_Vset_subset_lemma = result();
    63 
    66 
    64 val counit2_Int_Vset_subset = standard
    67 val counit2_Int_Vset_subset = standard
    65 	(counit2_Int_Vset_subset_lemma RS spec RS spec RS mp);
    68 	(counit2_Int_Vset_subset_lemma RS spec RS spec RS mp);