src/HOL/Finite_Set.thy

     (setprod f (A Un B) :: 'a ::{field})
       = setprod f A * setprod f B / setprod f (A Int B)"
   apply (subst setprod_Un_Int [symmetric], auto)
   apply (subgoal_tac "finite (A Int B)")
   apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
-  apply (subst times_divide_eq_right [THEN sym], auto)
+  apply (subst times_divide_eq_right [THEN sym], auto simp add: divide_self)
   done
 
 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
     (setprod f (A - {a}) :: 'a :: {field}) =
       (if a:A then setprod f A / f a else setprod f A)"
   apply (erule finite_induct)
    apply (auto simp add: insert_Diff_if)
   apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a")
   apply (erule ssubst)
   apply (subst times_divide_eq_right [THEN sym])
-  apply (auto simp add: mult_ac)
+  apply (auto simp add: mult_ac divide_self)
   done
 
 lemma setprod_inversef: "finite A ==>
     ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
       setprod (inverse \<circ> f) A = inverse (setprod f A)"