--- a/src/ZF/Sum.thy Sun Oct 07 15:49:25 2007 +0200
+++ b/src/ZF/Sum.thy Sun Oct 07 21:19:31 2007 +0200
@@ -196,55 +196,4 @@
lemma Part_sum_equality: "C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C"
by blast
-ML
-{*
-val sum_def = thm "sum_def";
-val Inl_def = thm "Inl_def";
-val Inr_def = thm "Inr_def";
-val sum_defs = thms "sum_defs";
-
-val Part_iff = thm "Part_iff";
-val Part_eqI = thm "Part_eqI";
-val PartI = thm "PartI";
-val PartE = thm "PartE";
-val Part_subset = thm "Part_subset";
-val Sigma_bool = thm "Sigma_bool";
-val InlI = thm "InlI";
-val InrI = thm "InrI";
-val sumE = thm "sumE";
-val Inl_iff = thm "Inl_iff";
-val Inr_iff = thm "Inr_iff";
-val Inl_Inr_iff = thm "Inl_Inr_iff";
-val Inr_Inl_iff = thm "Inr_Inl_iff";
-val sum_empty = thm "sum_empty";
-val Inl_inject = thm "Inl_inject";
-val Inr_inject = thm "Inr_inject";
-val Inl_neq_Inr = thm "Inl_neq_Inr";
-val Inr_neq_Inl = thm "Inr_neq_Inl";
-val InlD = thm "InlD";
-val InrD = thm "InrD";
-val sum_iff = thm "sum_iff";
-val sum_subset_iff = thm "sum_subset_iff";
-val sum_equal_iff = thm "sum_equal_iff";
-val sum_eq_2_times = thm "sum_eq_2_times";
-val case_Inl = thm "case_Inl";
-val case_Inr = thm "case_Inr";
-val case_type = thm "case_type";
-val expand_case = thm "expand_case";
-val case_cong = thm "case_cong";
-val case_case = thm "case_case";
-val Part_mono = thm "Part_mono";
-val Part_Collect = thm "Part_Collect";
-val Part_CollectE = thm "Part_CollectE";
-val Part_Inl = thm "Part_Inl";
-val Part_Inr = thm "Part_Inr";
-val PartD1 = thm "PartD1";
-val Part_id = thm "Part_id";
-val Part_Inr2 = thm "Part_Inr2";
-val Part_sum_equality = thm "Part_sum_equality";
-
-*}
-
-
-
end