src/HOL/Finite_Set.ML
changeset 15402 97204f3b4705
parent 15392 290bc97038c7
child 16733 236dfafbeb63
     1.1 --- a/src/HOL/Finite_Set.ML	Fri Dec 10 22:33:16 2004 +0100
     1.2 +++ b/src/HOL/Finite_Set.ML	Sun Dec 12 16:25:47 2004 +0100
     1.3 @@ -11,16 +11,6 @@
     1.4    val [emptyI, insertI] = thms "Finites.intros";
     1.5  end;
     1.6  
     1.7 -structure cardR =
     1.8 -struct
     1.9 -  val intrs = thms "cardR.intros";
    1.10 -  val elims = thms "cardR.cases";
    1.11 -  val elim = thm "cardR.cases";
    1.12 -  val induct = thm "cardR.induct";
    1.13 -  val mk_cases = InductivePackage.the_mk_cases (the_context ()) "Finite_Set.cardR";
    1.14 -  val [EmptyI, InsertI] = thms "cardR.intros";
    1.15 -end;
    1.16 -
    1.17  structure foldSet =
    1.18  struct
    1.19    val intrs = thms "foldSet.intros";
    1.20 @@ -31,11 +21,6 @@
    1.21    val [emptyI, insertI] = thms "foldSet.intros";
    1.22  end;
    1.23  
    1.24 -val cardR_SucD = thm "cardR_SucD";
    1.25 -val cardR_determ = thm "cardR_determ";
    1.26 -val cardR_emptyE = thm "cardR_emptyE";
    1.27 -val cardR_imp_finite = thm "cardR_imp_finite";
    1.28 -val cardR_insertE = thm "cardR_insertE";
    1.29  val card_0_eq = thm "card_0_eq";
    1.30  val card_Diff1_le = thm "card_Diff1_le";
    1.31  val card_Diff1_less = thm "card_Diff1_less";
    1.32 @@ -50,7 +35,6 @@
    1.33  val card_bij_eq = thm "card_bij_eq";
    1.34  val card_def = thm "card_def";
    1.35  val card_empty = thm "card_empty";
    1.36 -val card_equality = thm "card_equality";
    1.37  val card_eq_setsum = thm "card_eq_setsum";
    1.38  val card_image = thm "card_image";
    1.39  val card_image_le = thm "card_image_le";
    1.40 @@ -87,7 +71,6 @@
    1.41  val finite_empty_induct = thm "finite_empty_induct";
    1.42  val finite_imageD = thm "finite_imageD";
    1.43  val finite_imageI = thm "finite_imageI";
    1.44 -val finite_imp_cardR = thm "finite_imp_cardR";
    1.45  val finite_induct = thm "finite_induct";
    1.46  val finite_insert = thm "finite_insert";
    1.47  val finite_range_imageI = thm "finite_range_imageI";