src/HOL/Finite_Set.ML
changeset 14485 ea2707645af8
parent 12693 827818b891c7
child 15376 302ef111b621
     1.1 --- a/src/HOL/Finite_Set.ML	Thu Mar 25 10:31:25 2004 +0100
     1.2 +++ b/src/HOL/Finite_Set.ML	Thu Mar 25 10:32:21 2004 +0100
     1.3 @@ -32,7 +32,6 @@
     1.4  end;
     1.5  
     1.6  val Diff1_foldSet = thm "Diff1_foldSet";
     1.7 -val bounded_nat_set_is_finite = thm "bounded_nat_set_is_finite";
     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 @@ -83,7 +82,6 @@
    1.12  val finite_UN_I = thm "finite_UN_I";
    1.13  val finite_Un = thm "finite_Un";
    1.14  val finite_UnI = thm "finite_UnI";
    1.15 -val finite_atMost = thm "finite_atMost";
    1.16  val finite_converse = thm "finite_converse";
    1.17  val finite_empty_induct = thm "finite_empty_induct";
    1.18  val finite_imageD = thm "finite_imageD";
    1.19 @@ -92,7 +90,6 @@
    1.20  val finite_imp_foldSet = thm "finite_imp_foldSet";
    1.21  val finite_induct = thm "finite_induct";
    1.22  val finite_insert = thm "finite_insert";
    1.23 -val finite_lessThan = thm "finite_lessThan";
    1.24  val finite_range_imageI = thm "finite_range_imageI";
    1.25  val finite_subset = thm "finite_subset";
    1.26  val finite_subset_induct = thm "finite_subset_induct";