src/HOL/Datatype.thy
changeset 22230 bdec4a82f385
parent 21905 500f91bf992c
child 22424 8a5412121687
     1.1 --- a/src/HOL/Datatype.thy	Thu Feb 01 20:59:50 2007 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Fri Feb 02 15:47:58 2007 +0100
     1.3 @@ -558,6 +558,9 @@
     1.4    inject Inl_eq Inr_eq
     1.5    induction sum_induct
     1.6  
     1.7 +lemma sum_case_KK[simp]: "sum_case (%x. a) (%x. a) = (%x. a)"
     1.8 +  by (rule ext) (simp split: sum.split)
     1.9 +
    1.10  lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)"
    1.11    apply (rule_tac s = s in sumE)
    1.12     apply (erule ssubst)