src/ZF/Sum.thy
changeset 24893 b8ef7afe3a6b
parent 16417 9bc16273c2d4
child 32960 69916a850301
     1.1 --- a/src/ZF/Sum.thy	Sun Oct 07 15:49:25 2007 +0200
     1.2 +++ b/src/ZF/Sum.thy	Sun Oct 07 21:19:31 2007 +0200
     1.3 @@ -196,55 +196,4 @@
     1.4  lemma Part_sum_equality: "C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C"
     1.5  by blast
     1.6  
     1.7 -ML
     1.8 -{*
     1.9 -val sum_def = thm "sum_def";
    1.10 -val Inl_def = thm "Inl_def";
    1.11 -val Inr_def = thm "Inr_def";
    1.12 -val sum_defs = thms "sum_defs";
    1.13 -
    1.14 -val Part_iff = thm "Part_iff";
    1.15 -val Part_eqI = thm "Part_eqI";
    1.16 -val PartI = thm "PartI";
    1.17 -val PartE = thm "PartE";
    1.18 -val Part_subset = thm "Part_subset";
    1.19 -val Sigma_bool = thm "Sigma_bool";
    1.20 -val InlI = thm "InlI";
    1.21 -val InrI = thm "InrI";
    1.22 -val sumE = thm "sumE";
    1.23 -val Inl_iff = thm "Inl_iff";
    1.24 -val Inr_iff = thm "Inr_iff";
    1.25 -val Inl_Inr_iff = thm "Inl_Inr_iff";
    1.26 -val Inr_Inl_iff = thm "Inr_Inl_iff";
    1.27 -val sum_empty = thm "sum_empty";
    1.28 -val Inl_inject = thm "Inl_inject";
    1.29 -val Inr_inject = thm "Inr_inject";
    1.30 -val Inl_neq_Inr = thm "Inl_neq_Inr";
    1.31 -val Inr_neq_Inl = thm "Inr_neq_Inl";
    1.32 -val InlD = thm "InlD";
    1.33 -val InrD = thm "InrD";
    1.34 -val sum_iff = thm "sum_iff";
    1.35 -val sum_subset_iff = thm "sum_subset_iff";
    1.36 -val sum_equal_iff = thm "sum_equal_iff";
    1.37 -val sum_eq_2_times = thm "sum_eq_2_times";
    1.38 -val case_Inl = thm "case_Inl";
    1.39 -val case_Inr = thm "case_Inr";
    1.40 -val case_type = thm "case_type";
    1.41 -val expand_case = thm "expand_case";
    1.42 -val case_cong = thm "case_cong";
    1.43 -val case_case = thm "case_case";
    1.44 -val Part_mono = thm "Part_mono";
    1.45 -val Part_Collect = thm "Part_Collect";
    1.46 -val Part_CollectE = thm "Part_CollectE";
    1.47 -val Part_Inl = thm "Part_Inl";
    1.48 -val Part_Inr = thm "Part_Inr";
    1.49 -val PartD1 = thm "PartD1";
    1.50 -val Part_id = thm "Part_id";
    1.51 -val Part_Inr2 = thm "Part_Inr2";
    1.52 -val Part_sum_equality = thm "Part_sum_equality";
    1.53 -
    1.54 -*}
    1.55 -
    1.56 -
    1.57 -
    1.58  end