src/HOL/Sum_Type.thy
changeset 27104 791607529f6d
parent 25534 d0b74fdd6067
child 28524 644b62cf678f
     1.1 --- a/src/HOL/Sum_Type.thy	Tue Jun 10 15:30:06 2008 +0200
     1.2 +++ b/src/HOL/Sum_Type.thy	Tue Jun 10 15:30:33 2008 +0200
     1.3 @@ -171,9 +171,6 @@
     1.4  apply (auto simp add: Sum_def Inl_def Inr_def)
     1.5  done
     1.6  
     1.7 -lemma sum_induct: "[| !!x. P (Inl x); !!x. P (Inr x) |] ==> P x"
     1.8 -by (rule sumE [of x], auto)
     1.9 -
    1.10  
    1.11  lemma UNIV_Plus_UNIV [simp]: "UNIV <+> UNIV = UNIV"
    1.12  apply (rule set_ext)
    1.13 @@ -237,7 +234,6 @@
    1.14  val InrI = thm "InrI";
    1.15  val PlusE = thm "PlusE";
    1.16  val sumE = thm "sumE";
    1.17 -val sum_induct = thm "sum_induct";
    1.18  val Part_eqI = thm "Part_eqI";
    1.19  val PartI = thm "PartI";
    1.20  val PartE = thm "PartE";