--- a/src/HOL/Analysis/Infinite_Set_Sum.thy Sat Oct 30 19:41:09 2021 +0200
+++ b/src/HOL/Analysis/Infinite_Set_Sum.thy Sat Oct 30 19:58:45 2021 +0200
@@ -1242,7 +1242,7 @@
moreover have "Sup {y. \<exists>x. (\<exists>y. finite y \<and> y \<subseteq> A \<and> x = ennreal (sum f y)) \<and>
y = enn2ereal x} = Sup {y. \<exists>x. finite x \<and> x \<subseteq> A \<and> y = ereal (sum f x)}"
using enn2ereal_ennreal fnn in_mono sum_nonneg Collect_cong
- by smt
+ by (smt (verit, ccfv_SIG))
ultimately show "max 0 (Sup {y. \<exists>x. (\<exists>xa. finite xa \<and> xa \<subseteq> A \<and> x
= ennreal (sum f xa)) \<and> y = enn2ereal x})
= Sup {y. \<exists>x. finite x \<and> x \<subseteq> A \<and> y = ereal (sum f x)}"
--- a/src/HOL/Analysis/Infinite_Sum.thy Sat Oct 30 19:41:09 2021 +0200
+++ b/src/HOL/Analysis/Infinite_Sum.thy Sat Oct 30 19:58:45 2021 +0200
@@ -511,7 +511,7 @@
and "finite F" and "F \<subseteq> A"
by (simp add: atomize_elim)
hence "norm a \<le> norm (sum f F) + \<epsilon>"
- by (smt norm_triangle_sub)
+ by (metis add.commute diff_add_cancel dual_order.refl norm_triangle_mono)
also have "\<dots> \<le> sum (\<lambda>x. norm (f x)) F + \<epsilon>"
using norm_sum by auto
also have "\<dots> \<le> n + \<epsilon>"
@@ -570,7 +570,7 @@
by blast
hence "(\<Sum>x\<in>X. norm (f x)) < 0"
unfolding S_def by auto
- thus False using sumpos by smt
+ thus False by (simp add: leD sumpos)
qed
have "\<exists>!h. (sum (\<lambda>x. norm (f x)) \<longlongrightarrow> h) (finite_subsets_at_top A)"
using t_def finite_subsets_at_top_neq_bot tendsto_unique by blast