# HG changeset patch
# User huffman
# Date 1338283813 -7200
# Node ID 391439b10100642f2016966b6da00a75763c7dd9
# Parent  0da831254551aabd743d2be824317e48973850d7
remove unused intermediate lemma

diff -r 0da831254551 -r 391439b10100 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue May 29 11:13:00 2012 +0200
+++ b/src/HOL/Library/Multiset.thy	Tue May 29 11:30:13 2012 +0200
@@ -539,14 +539,6 @@
 
 subsection {* Induction and case splits *}
 
-lemma setsum_decr:
-  "finite F ==> (0::nat) < f a ==>
-    setsum (f (a := f a - 1)) F = (if a\<in>F then setsum f F - 1 else setsum f F)"
-apply (induct rule: finite_induct)
- apply auto
-apply (drule_tac a = a in mk_disjoint_insert, auto)
-done
-
 theorem multiset_induct [case_names empty add, induct type: multiset]:
   assumes empty: "P {#}"
   assumes add: "\<And>M x. P M \<Longrightarrow> P (M + {#x#})"