equal
deleted
inserted
replaced
330 by (resolve_tac prems 1); |
330 by (resolve_tac prems 1); |
331 by (rtac ext 1); |
331 by (rtac ext 1); |
332 by (Force_tac 1); |
332 by (Force_tac 1); |
333 by (Clarify_tac 1); |
333 by (Clarify_tac 1); |
334 by (ftac setsum_SucD 1); |
334 by (ftac setsum_SucD 1); |
335 by (assume_tac 1); |
|
336 by (Clarify_tac 1); |
335 by (Clarify_tac 1); |
337 by (rename_tac "a" 1); |
336 by (rename_tac "a" 1); |
338 by (subgoal_tac "finite{x. 0 < (f(a:=f(a)-1)) x}" 1); |
337 by (subgoal_tac "finite{x. 0 < (f(a:=f(a)-1)) x}" 1); |
339 by (etac (rotate_prems 1 finite_subset) 2); |
338 by (etac (rotate_prems 1 finite_subset) 2); |
340 by (Simp_tac 2); |
339 by (Simp_tac 2); |