equal
deleted
inserted
replaced
307 prefer 2 |
307 prefer 2 |
308 apply blast |
308 apply blast |
309 apply (subgoal_tac "{x. x \<noteq> a \<and> 0 < f x} = {x. 0 < f x} - {a}") |
309 apply (subgoal_tac "{x. x \<noteq> a \<and> 0 < f x} = {x. 0 < f x} - {a}") |
310 prefer 2 |
310 prefer 2 |
311 apply blast |
311 apply blast |
312 apply (simp add: le_imp_diff_is_add setsum_diff1 cong: conj_cong) |
312 apply (simp add: le_imp_diff_is_add setsum_diff1_nat cong: conj_cong) |
313 done |
313 done |
314 qed |
314 qed |
315 |
315 |
316 theorem rep_multiset_induct: |
316 theorem rep_multiset_induct: |
317 "f \<in> multiset ==> P (\<lambda>a. 0) ==> |
317 "f \<in> multiset ==> P (\<lambda>a. 0) ==> |