equal
deleted
inserted
replaced
325 by(subgoal_tac "{x. x ~= a --> 0 < f x} = {x. 0 < f x}" 1); |
325 by(subgoal_tac "{x. x ~= a --> 0 < f x} = {x. 0 < f x}" 1); |
326 by(Blast_tac 2); |
326 by(Blast_tac 2); |
327 by(subgoal_tac "{x. x ~= a & 0 < f x} = {x. 0 < f x} - {a}" 1); |
327 by(subgoal_tac "{x. x ~= a & 0 < f x} = {x. 0 < f x} - {a}" 1); |
328 by(Blast_tac 2); |
328 by(Blast_tac 2); |
329 by(asm_simp_tac (simpset() addsimps [le_imp_diff_is_add,setsum_diff1] |
329 by(asm_simp_tac (simpset() addsimps [le_imp_diff_is_add,setsum_diff1] |
330 addcongs [conj_cong] |
330 addcongs [conj_cong]) 1); |
331 addSolver cut_trans_tac) 1); |
|
332 val lemma = result(); |
331 val lemma = result(); |
333 |
332 |
334 val major::prems = Goal |
333 val major::prems = Goal |
335 "[| f : multiset; \ |
334 "[| f : multiset; \ |
336 \ P(%a.0); \ |
335 \ P(%a.0); \ |