src/HOL/Datatype.thy
changeset 25672 5850301e83c7
parent 25534 d0b74fdd6067
child 25836 f7771e4f7064
     1.1 --- a/src/HOL/Datatype.thy	Mon Dec 17 18:11:21 2007 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Mon Dec 17 18:22:48 2007 +0100
     1.3 @@ -541,9 +541,6 @@
     1.4    inject Inl_eq Inr_eq
     1.5    induction sum_induct
     1.6  
     1.7 -lemma size_sum [code func]:
     1.8 -  "size (x \<Colon> 'a + 'b) = 0" by (cases x) auto
     1.9 -
    1.10  lemma sum_case_KK[simp]: "sum_case (%x. a) (%x. a) = (%x. a)"
    1.11    by (rule ext) (simp split: sum.split)
    1.12