src/HOL/Induct/Multiset.ML

   by (Asm_simp_tac 1);
   by (resolve_tac prems 1);
  by (rtac ext 1);
  by (Force_tac 1);
 by (Clarify_tac 1);
-by (forward_tac [setsum_SucD] 1);
+by (ftac setsum_SucD 1);
  by (assume_tac 1);
 by (Clarify_tac 1);
 by (rename_tac "a" 1);
 by (subgoal_tac "finite{x. 0 < (f(a:=f(a)-1)) x}" 1);
  by (etac (rotate_prems 1 finite_subset) 2);