diff -r ef8c7c5eb01b -r ea2707645af8 src/HOL/Finite_Set.ML
--- a/src/HOL/Finite_Set.ML	Thu Mar 25 10:31:25 2004 +0100
+++ b/src/HOL/Finite_Set.ML	Thu Mar 25 10:32:21 2004 +0100
@@ -32,7 +32,6 @@
 end;
 
 val Diff1_foldSet = thm "Diff1_foldSet";
-val bounded_nat_set_is_finite = thm "bounded_nat_set_is_finite";
 val cardR_SucD = thm "cardR_SucD";
 val cardR_determ = thm "cardR_determ";
 val cardR_emptyE = thm "cardR_emptyE";
@@ -83,7 +82,6 @@
 val finite_UN_I = thm "finite_UN_I";
 val finite_Un = thm "finite_Un";
 val finite_UnI = thm "finite_UnI";
-val finite_atMost = thm "finite_atMost";
 val finite_converse = thm "finite_converse";
 val finite_empty_induct = thm "finite_empty_induct";
 val finite_imageD = thm "finite_imageD";
@@ -92,7 +90,6 @@
 val finite_imp_foldSet = thm "finite_imp_foldSet";
 val finite_induct = thm "finite_induct";
 val finite_insert = thm "finite_insert";
-val finite_lessThan = thm "finite_lessThan";
 val finite_range_imageI = thm "finite_range_imageI";
 val finite_subset = thm "finite_subset";
 val finite_subset_induct = thm "finite_subset_induct";