author | lcp |
Mon, 15 Aug 1994 18:31:29 +0200 | |
changeset 527 | 35c70ab82940 |
parent 526 | 85d7ff169b9c |
child 528 | 61dc99226f8f |
--- a/src/ZF/ex/CoUnit.ML Mon Aug 15 18:27:50 1994 +0200 +++ b/src/ZF/ex/CoUnit.ML Mon Aug 15 18:31:29 1994 +0200 @@ -58,6 +58,9 @@ by (etac counit2.elim 1); by (etac counit2.elim 1); by (rewrite_goals_tac counit2.con_defs); +val lleq_cs = subset_cs + addSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono] + addSEs [Ord_in_Ord, Pair_inject]; by (fast_tac lleq_cs 1); val counit2_Int_Vset_subset_lemma = result();