src/ZF/InfDatatype.ML
changeset 768 59c0a821e468
parent 760 f0200e91b272
child 801 316121afb5b5
equal deleted inserted replaced
767:a4fce3b94065 768:59c0a821e468
   174                               |> standard;
   174                               |> standard;
   175 
   175 
   176 val le_nat_Un_cardinal = 
   176 val le_nat_Un_cardinal = 
   177     [Ord_nat, Card_cardinal RS Card_is_Ord] MRS Un_upper2_le  |> standard;
   177     [Ord_nat, Card_cardinal RS Card_is_Ord] MRS Un_upper2_le  |> standard;
   178 
   178 
   179 val UN_upper_cardinal = UN_upper RS subset_imp_lepoll RS lepoll_imp_le 
   179 val UN_upper_cardinal = UN_upper RS subset_imp_lepoll RS lepoll_imp_Card_le 
   180                         |> standard;
   180                         |> standard;
   181 
   181 
   182 (*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *)
   182 (*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *)
   183 val inf_datatype_intrs =  
   183 val inf_datatype_intrs =  
   184     [InfCard_nat, InfCard_nat_Un_cardinal,
   184     [InfCard_nat, InfCard_nat_Un_cardinal,