remove unused intermediate lemma
authorhuffman
Tue May 29 11:30:13 2012 +0200 (2012-05-29)
changeset 48011391439b10100
parent 48010 0da831254551
child 48012 b6e5e86a7303
remove unused intermediate lemma
src/HOL/Library/Multiset.thy
     1.1 --- a/src/HOL/Library/Multiset.thy	Tue May 29 11:13:00 2012 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Tue May 29 11:30:13 2012 +0200
     1.3 @@ -539,14 +539,6 @@
     1.4  
     1.5  subsection {* Induction and case splits *}
     1.6  
     1.7 -lemma setsum_decr:
     1.8 -  "finite F ==> (0::nat) < f a ==>
     1.9 -    setsum (f (a := f a - 1)) F = (if a\<in>F then setsum f F - 1 else setsum f F)"
    1.10 -apply (induct rule: finite_induct)
    1.11 - apply auto
    1.12 -apply (drule_tac a = a in mk_disjoint_insert, auto)
    1.13 -done
    1.14 -
    1.15  theorem multiset_induct [case_names empty add, induct type: multiset]:
    1.16    assumes empty: "P {#}"
    1.17    assumes add: "\<And>M x. P M \<Longrightarrow> P (M + {#x#})"