author | lcp |
Thu, 08 Dec 1994 14:18:31 +0100 (1994-12-08) | |
changeset 768 | 59c0a821e468 |
parent 767 | a4fce3b94065 |
child 769 | 66cdfde4ec5d |
--- 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)) *)