UN_upper_cardinal: updated to refer to Card_le_imp_lepoll
authorlcp
Thu, 08 Dec 1994 14:18:31 +0100 (1994-12-08)
changeset 768 59c0a821e468
parent 767 a4fce3b94065
child 769 66cdfde4ec5d
UN_upper_cardinal: updated to refer to Card_le_imp_lepoll and lepoll_imp_Card_le
src/ZF/InfDatatype.ML
--- a/src/ZF/InfDatatype.ML	Thu Dec 08 14:06:16 1994 +0100
+++ b/src/ZF/InfDatatype.ML	Thu Dec 08 14:18:31 1994 +0100
@@ -176,7 +176,7 @@
 val le_nat_Un_cardinal = 
     [Ord_nat, Card_cardinal RS Card_is_Ord] MRS Un_upper2_le  |> standard;
 
-val UN_upper_cardinal = UN_upper RS subset_imp_lepoll RS lepoll_imp_le 
+val UN_upper_cardinal = UN_upper RS subset_imp_lepoll RS lepoll_imp_Card_le 
                         |> standard;
 
 (*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *)