equal
deleted
inserted
replaced
101 lemmas InfCard_nat_Un_cardinal = InfCard_Un [OF InfCard_nat Card_cardinal] |
101 lemmas InfCard_nat_Un_cardinal = InfCard_Un [OF InfCard_nat Card_cardinal] |
102 |
102 |
103 lemmas le_nat_Un_cardinal = |
103 lemmas le_nat_Un_cardinal = |
104 Un_upper2_le [OF Ord_nat Card_cardinal [THEN Card_is_Ord]] |
104 Un_upper2_le [OF Ord_nat Card_cardinal [THEN Card_is_Ord]] |
105 |
105 |
106 lemmas UN_upper_cardinal = UN_upper [THEN subset_imp_lepoll, THEN lepoll_imp_Card_le] |
106 lemmas UN_upper_cardinal = UN_upper [THEN subset_imp_lepoll, THEN lepoll_imp_cardinal_le] |
107 |
107 |
108 (*The new version of Data_Arg.intrs, declared in Datatype.ML*) |
108 (*The new version of Data_Arg.intrs, declared in Datatype.ML*) |
109 lemmas Data_Arg_intros = |
109 lemmas Data_Arg_intros = |
110 SigmaI InlI InrI |
110 SigmaI InlI InrI |
111 Pair_in_univ Inl_in_univ Inr_in_univ |
111 Pair_in_univ Inl_in_univ Inr_in_univ |