src/ZF/ex/CoUnit.ML

--- 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();