src/HOL/Finite_Set.ML
changeset 15392 290bc97038c7
parent 15376 302ef111b621
child 15402 97204f3b4705
     1.1 --- a/src/HOL/Finite_Set.ML	Thu Dec 09 16:45:46 2004 +0100
     1.2 +++ b/src/HOL/Finite_Set.ML	Thu Dec 09 18:30:59 2004 +0100
     1.3 @@ -31,7 +31,6 @@
     1.4    val [emptyI, insertI] = thms "foldSet.intros";
     1.5  end;
     1.6  
     1.7 -val Diff1_foldSet = thm "Diff1_foldSet";
     1.8  val cardR_SucD = thm "cardR_SucD";
     1.9  val cardR_determ = thm "cardR_determ";
    1.10  val cardR_emptyE = thm "cardR_emptyE";
    1.11 @@ -51,8 +50,8 @@
    1.12  val card_bij_eq = thm "card_bij_eq";
    1.13  val card_def = thm "card_def";
    1.14  val card_empty = thm "card_empty";
    1.15 +val card_equality = thm "card_equality";
    1.16  val card_eq_setsum = thm "card_eq_setsum";
    1.17 -val card_equality = thm "card_equality";
    1.18  val card_image = thm "card_image";
    1.19  val card_image_le = thm "card_image_le";
    1.20  val card_inj_on_le = thm "card_inj_on_le";
    1.21 @@ -66,6 +65,7 @@
    1.22  val card_seteq = thm "card_seteq";
    1.23  val choose_deconstruct = thm "choose_deconstruct";
    1.24  val constr_bij = thm "constr_bij";
    1.25 +val Diff1_foldSet = thm "Diff1_foldSet";
    1.26  val dvd_partition = thm "dvd_partition";
    1.27  val empty_foldSetE = thm "empty_foldSetE";
    1.28  val endo_inj_surj = thm "endo_inj_surj";
    1.29 @@ -74,6 +74,7 @@
    1.30  val finite_Diff = thm "finite_Diff";
    1.31  val finite_Diff_insert = thm "finite_Diff_insert";
    1.32  val finite_Field = thm "finite_Field";
    1.33 +val finite_imp_foldSet = thm "finite_imp_foldSet";
    1.34  val finite_Int = thm "finite_Int";
    1.35  val finite_Pow_iff = thm "finite_Pow_iff";
    1.36  val finite_Prod_UNIV = thm "finite_Prod_UNIV";
    1.37 @@ -87,25 +88,24 @@
    1.38  val finite_imageD = thm "finite_imageD";
    1.39  val finite_imageI = thm "finite_imageI";
    1.40  val finite_imp_cardR = thm "finite_imp_cardR";
    1.41 -val finite_imp_foldSet = thm "finite_imp_foldSet";
    1.42  val finite_induct = thm "finite_induct";
    1.43  val finite_insert = thm "finite_insert";
    1.44  val finite_range_imageI = thm "finite_range_imageI";
    1.45  val finite_subset = thm "finite_subset";
    1.46  val finite_subset_induct = thm "finite_subset_induct";
    1.47  val finite_trancl = thm "finite_trancl";
    1.48 -val foldSet_determ = thm "LC.foldSet_determ";
    1.49 +val foldSet_determ = thm "ACf.foldSet_determ";
    1.50  val foldSet_imp_finite = thm "foldSet_imp_finite";
    1.51  val fold_Un_Int = thm "ACe.fold_Un_Int";
    1.52  val fold_Un_disjoint = thm "ACe.fold_Un_disjoint";
    1.53 -val fold_Un_disjoint2 = thm "ACe.fold_o_Un_disjoint";
    1.54 -val fold_commute = thm "LC.fold_commute";
    1.55 +val fold_Un_disjoint2 = thm "ACe.fold_Un_disjoint";
    1.56 +val fold_commute = thm "ACf.fold_commute";
    1.57  val fold_def = thm "fold_def";
    1.58  val fold_empty = thm "fold_empty";
    1.59 -val fold_equality = thm "LC.fold_equality";
    1.60 -val fold_insert = thm "LC.fold_insert";
    1.61 -val fold_nest_Un_Int = thm "LC.fold_nest_Un_Int";
    1.62 -val fold_nest_Un_disjoint = thm "LC.fold_nest_Un_disjoint";
    1.63 +val fold_equality = thm "ACf.fold_equality";
    1.64 +val fold_insert = thm "ACf.fold_insert";
    1.65 +val fold_nest_Un_Int = thm "ACf.fold_nest_Un_Int";
    1.66 +val fold_nest_Un_disjoint = thm "ACf.fold_nest_Un_disjoint";
    1.67  val n_sub_lemma = thm "n_sub_lemma";
    1.68  val n_subsets = thm "n_subsets";
    1.69  val psubset_card_mono = thm "psubset_card_mono";