# HG changeset patch
# User berghofe
# Date 1197912168 -3600
# Node ID 5850301e83c7f8077ac028618def60f7bc125721
# Parent  5e9d6f77d11afd911833d810a27382410c193b0c
Removed obsolete lemma size_sum.

diff -r 5e9d6f77d11a -r 5850301e83c7 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Mon Dec 17 18:11:21 2007 +0100
+++ b/src/HOL/Datatype.thy	Mon Dec 17 18:22:48 2007 +0100
@@ -541,9 +541,6 @@
   inject Inl_eq Inr_eq
   induction sum_induct
 
-lemma size_sum [code func]:
-  "size (x \<Colon> 'a + 'b) = 0" by (cases x) auto
-
 lemma sum_case_KK[simp]: "sum_case (%x. a) (%x. a) = (%x. a)"
   by (rule ext) (simp split: sum.split)