src/HOL/Analysis/Caratheodory.thy

         moreover
         have Ai_eq: "A i = (\<Union>x<card C. f x)"
           using f C Ai unfolding bij_betw_def by auto
         then have "\<Union>range f = A i"
           using f C Ai unfolding bij_betw_def
-            by (auto simp add: f_def cong del: SUP_cong_strong)
+            by (auto simp add: f_def cong del: SUP_cong_simp)
         moreover
         { have "(\<Sum>j. \<mu>_r (f j)) = (\<Sum>j. if j \<in> {..< card C} then \<mu>_r (f j) else 0)"
             using volume_empty[OF V(1)] by (auto intro!: arg_cong[where f=suminf] simp: f_def)
           also have "\<dots> = (\<Sum>j<card C. \<mu>_r (f j))"
             by (rule sums_If_finite_set[THEN sums_unique, symmetric]) simp