# File Finite_Set.ML

    (* legacy ML bindings *)

    structure Finites =
    struct
      val intrs = thms "Finites.intros";
      val elims = thms "Finites.cases";
      val elim = thm "Finites.cases";
      val induct = thm "Finites.induct";
      val mk_cases = InductivePackage.the_mk_cases (the_context ()) "Finite_Set.Finites";
      val [emptyI, insertI] = thms "Finites.intros";
    end;

    structure foldSet =
    struct
      val intrs = thms "foldSet.intros";
      val elims = thms "foldSet.cases";
      val elim = thm "foldSet.cases";
      val induct = thm "foldSet.induct";
      val mk_cases = InductivePackage.the_mk_cases (the_context ()) "Finite_Set.foldSet";
      val [emptyI, insertI] = thms "foldSet.intros";
    end;

    val card_0_eq = thm "card_0_eq";
    val card_Diff1_le = thm "card_Diff1_le";
    val card_Diff1_less = thm "card_Diff1_less";
    val card_Diff2_less = thm "card_Diff2_less";
    val card_Diff_singleton = thm "card_Diff_singleton";
    val card_Diff_singleton_if = thm "card_Diff_singleton_if";
    val card_Diff_subset = thm "card_Diff_subset";
    val card_Pow = thm "card_Pow";
    val card_Suc_Diff1 = thm "card_Suc_Diff1";
    val card_Un_Int = thm "card_Un_Int";
    val card_Un_disjoint = thm "card_Un_disjoint";
    val card_bij_eq = thm "card_bij_eq";
    val card_def = thm "card_def";
    val card_empty = thm "card_empty";
    val card_eq_setsum = thm "card_eq_setsum";
    val card_image = thm "card_image";
    val card_image_le = thm "card_image_le";
    val card_inj_on_le = thm "card_inj_on_le";
    val card_insert = thm "card_insert";
    val card_insert_disjoint = thm "card_insert_disjoint";
    val card_insert_if = thm "card_insert_if";
    val card_insert_le = thm "card_insert_le";
    val card_mono = thm "card_mono";
    val card_psubset = thm "card_psubset";
    val card_seteq = thm "card_seteq";
    val Diff1_foldSet = thm "Diff1_foldSet";
    val dvd_partition = thm "dvd_partition";
    val empty_foldSetE = thm "empty_foldSetE";
    val endo_inj_surj = thm "endo_inj_surj";
    val finite = thm "finite";
    val finite_Diff = thm "finite_Diff";
    val finite_Diff_insert = thm "finite_Diff_insert";
    val finite_Field = thm "finite_Field";
    val finite_imp_foldSet = thm "finite_imp_foldSet";
    val finite_Int = thm "finite_Int";
    val finite_Pow_iff = thm "finite_Pow_iff";
    val finite_Prod_UNIV = thm "finite_Prod_UNIV";
    val finite_SigmaI = thm "finite_SigmaI";
    val finite_UN = thm "finite_UN";
    val finite_UN_I = thm "finite_UN_I";
    val finite_Un = thm "finite_Un";
    val finite_UnI = thm "finite_UnI";
    val finite_converse = thm "finite_converse";
    val finite_empty_induct = thm "finite_empty_induct";
    val finite_imageD = thm "finite_imageD";
    val finite_imageI = thm "finite_imageI";
    val finite_induct = thm "finite_induct";
    val finite_insert = thm "finite_insert";
    val finite_range_imageI = thm "finite_range_imageI";
    val finite_subset = thm "finite_subset";
    val finite_subset_induct = thm "finite_subset_induct";
    val finite_trancl = thm "finite_trancl";
    val foldSet_determ = thm "ACf.foldSet_determ";
    val foldSet_imp_finite = thm "foldSet_imp_finite";
    val fold_Un_Int = thm "ACe.fold_Un_Int";
    val fold_Un_disjoint = thm "ACe.fold_Un_disjoint";
    val fold_Un_disjoint2 = thm "ACe.fold_Un_disjoint";
    val fold_commute = thm "ACf.fold_commute";
    val fold_def = thm "fold_def";
    val fold_empty = thm "fold_empty";
    val fold_equality = thm "ACf.fold_equality";
    val fold_insert = thm "ACf.fold_insert";
    val fold_nest_Un_Int = thm "ACf.fold_nest_Un_Int";
    val fold_nest_Un_disjoint = thm "ACf.fold_nest_Un_disjoint";
    val psubset_card_mono = thm "psubset_card_mono";
    val setsum_0 = thm "setsum_0";
    val setsum_SucD = thm "setsum_SucD";
    val setsum_UN_disjoint = thm "setsum_UN_disjoint";
    val setsum_Un = thm "setsum_Un";
    val setsum_Un_Int = thm "setsum_Un_Int";
    val setsum_Un_disjoint = thm "setsum_Un_disjoint";
    val setsum_addf = thm "setsum_addf";
    val setsum_cong = thm "setsum_cong";
    val setsum_def = thm "setsum_def";
    val setsum_diff1 = thm "setsum_diff1";
    val setsum_empty = thm "setsum_empty";
    val setsum_eq_0_iff = thm "setsum_eq_0_iff";
    val setsum_insert = thm "setsum_insert";
    val trancl_subset_Field2 = thm "trancl_subset_Field2";