# HG changeset patch
# User haftmann
# Date 1285744080 -7200
# Node ID 9b1814140bcf95283a518f701744ff0a0f9f3df5
# Parent  4f8f08362bf76b97312b02d5c6b6d9b6272234ac
delete code lemma explicitly

diff -r 4f8f08362bf7 -r 9b1814140bcf src/HOL/Library/More_List.thy
--- a/src/HOL/Library/More_List.thy	Wed Sep 29 09:07:58 2010 +0200
+++ b/src/HOL/Library/More_List.thy	Wed Sep 29 09:08:00 2010 +0200
@@ -100,6 +100,8 @@
   "fold plus xs = plus (listsum (rev xs))"
   by (induct xs) (simp_all add: add.assoc)
 
+declare listsum_foldl [code del]
+
 lemma (in monoid_add) listsum_conv_fold [code]:
   "listsum xs = fold (\<lambda>x y. y + x) xs 0"
   by (auto simp add: listsum_foldl foldl_fold fun_eq_iff)