equal
deleted
inserted
replaced
43 val card_insert_disjoint = thm "card_insert_disjoint"; |
43 val card_insert_disjoint = thm "card_insert_disjoint"; |
44 val card_insert_if = thm "card_insert_if"; |
44 val card_insert_if = thm "card_insert_if"; |
45 val card_insert_le = thm "card_insert_le"; |
45 val card_insert_le = thm "card_insert_le"; |
46 val card_mono = thm "card_mono"; |
46 val card_mono = thm "card_mono"; |
47 val card_psubset = thm "card_psubset"; |
47 val card_psubset = thm "card_psubset"; |
48 val card_s_0_eq_empty = thm "card_s_0_eq_empty"; |
|
49 val card_seteq = thm "card_seteq"; |
48 val card_seteq = thm "card_seteq"; |
50 val choose_deconstruct = thm "choose_deconstruct"; |
|
51 val constr_bij = thm "constr_bij"; |
|
52 val Diff1_foldSet = thm "Diff1_foldSet"; |
49 val Diff1_foldSet = thm "Diff1_foldSet"; |
53 val dvd_partition = thm "dvd_partition"; |
50 val dvd_partition = thm "dvd_partition"; |
54 val empty_foldSetE = thm "empty_foldSetE"; |
51 val empty_foldSetE = thm "empty_foldSetE"; |
55 val endo_inj_surj = thm "endo_inj_surj"; |
52 val endo_inj_surj = thm "endo_inj_surj"; |
56 val finite = thm "finite"; |
53 val finite = thm "finite"; |
87 val fold_empty = thm "fold_empty"; |
84 val fold_empty = thm "fold_empty"; |
88 val fold_equality = thm "ACf.fold_equality"; |
85 val fold_equality = thm "ACf.fold_equality"; |
89 val fold_insert = thm "ACf.fold_insert"; |
86 val fold_insert = thm "ACf.fold_insert"; |
90 val fold_nest_Un_Int = thm "ACf.fold_nest_Un_Int"; |
87 val fold_nest_Un_Int = thm "ACf.fold_nest_Un_Int"; |
91 val fold_nest_Un_disjoint = thm "ACf.fold_nest_Un_disjoint"; |
88 val fold_nest_Un_disjoint = thm "ACf.fold_nest_Un_disjoint"; |
92 val n_sub_lemma = thm "n_sub_lemma"; |
|
93 val n_subsets = thm "n_subsets"; |
|
94 val psubset_card_mono = thm "psubset_card_mono"; |
89 val psubset_card_mono = thm "psubset_card_mono"; |
95 val setsum_0 = thm "setsum_0"; |
90 val setsum_0 = thm "setsum_0"; |
96 val setsum_SucD = thm "setsum_SucD"; |
91 val setsum_SucD = thm "setsum_SucD"; |
97 val setsum_UN_disjoint = thm "setsum_UN_disjoint"; |
92 val setsum_UN_disjoint = thm "setsum_UN_disjoint"; |
98 val setsum_Un = thm "setsum_Un"; |
93 val setsum_Un = thm "setsum_Un"; |