| changeset 39778 | 9b1814140bcf |
| parent 39773 | 38852e989efa |
| child 39791 | a91430778479 |
--- 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)