src/HOL/Integ/IntDef.thy

   apply (case_tac "finite A")
   apply (erule finite_induct, auto)
   done
 
 lemma int_setsum: "int (setsum f A) = setsum (int \<circ> f) A"
-  by (subst int_eq_of_nat, rule setsum_of_nat)
+  by (simp add: int_eq_of_nat setsum_of_nat) 
 
 lemma setprod_of_nat: "of_nat (setprod f A) = setprod (of_nat \<circ> f) A"
   apply (case_tac "finite A")
   apply (erule finite_induct, auto)
   done

   apply (case_tac "finite A")
   apply (erule finite_induct, auto)
   done
 
 lemma int_setprod: "int (setprod f A) = setprod (int \<circ> f) A"
-  by (subst int_eq_of_nat, rule setprod_of_nat)
+  by (simp add: int_eq_of_nat setprod_of_nat)
 
 lemma setsum_constant [simp]: "finite A ==> (\<Sum>x \<in> A. y) = of_nat(card A) * y"
   apply (erule finite_induct)
   apply (auto simp add: ring_distrib add_ac)
   done