--- a/src/HOL/Finite_Set.ML Thu Jul 07 12:36:56 2005 +0200
+++ b/src/HOL/Finite_Set.ML Thu Jul 07 12:39:17 2005 +0200
@@ -45,10 +45,7 @@
val card_insert_le = thm "card_insert_le";
val card_mono = thm "card_mono";
val card_psubset = thm "card_psubset";
-val card_s_0_eq_empty = thm "card_s_0_eq_empty";
val card_seteq = thm "card_seteq";
-val choose_deconstruct = thm "choose_deconstruct";
-val constr_bij = thm "constr_bij";
val Diff1_foldSet = thm "Diff1_foldSet";
val dvd_partition = thm "dvd_partition";
val empty_foldSetE = thm "empty_foldSetE";
@@ -89,8 +86,6 @@
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 n_sub_lemma = thm "n_sub_lemma";
-val n_subsets = thm "n_subsets";
val psubset_card_mono = thm "psubset_card_mono";
val setsum_0 = thm "setsum_0";
val setsum_SucD = thm "setsum_SucD";