# HG changeset patch
# User wenzelm
# Date 1635616725 -7200
# Node ID 8af77cb50c6d1f15cc13e56a855d06b434aa3ccf
# Parent  6f801e1073fa8f995362df2e12d48aba0057476e
tuned proofs -- avoid z3, which is unavailable on arm64-linux;

diff -r 6f801e1073fa -r 8af77cb50c6d src/HOL/Analysis/Infinite_Set_Sum.thy
--- 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)}"
diff -r 6f801e1073fa -r 8af77cb50c6d src/HOL/Analysis/Infinite_Sum.thy
--- 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