# HG changeset patch
# User wenzelm
# Date 1706136831 -3600
# Node ID cb933e165dc33831444d8c4ed66f5033b0b8a182
# Parent  667cb8b79909081d85e810b88012e1017aaa4d91
tuned proof: avoid z3 to make it work on arm64-linux;

diff -r 667cb8b79909 -r cb933e165dc3 src/HOL/Analysis/Infinite_Sum.thy
--- a/src/HOL/Analysis/Infinite_Sum.thy	Wed Jan 24 22:43:41 2024 +0100
+++ b/src/HOL/Analysis/Infinite_Sum.thy	Wed Jan 24 23:53:51 2024 +0100
@@ -2387,9 +2387,10 @@
 lemma (in uniform_space) cauchy_filter_iff:
   "cauchy_filter F \<longleftrightarrow> (\<forall>P. eventually P uniformity \<longrightarrow> (\<exists>X. eventually (\<lambda>x. x \<in> X) F \<and> (\<forall>z\<in>X\<times>X. P z)))" 
   unfolding cauchy_filter_def le_filter_def
-  apply auto
-   apply (smt (z3) eventually_mono eventually_prod_same mem_Collect_eq)
-  using eventually_prod_same by blast                            
+  apply (auto simp: eventually_prod_same)
+   apply (metis (full_types) eventually_mono mem_Collect_eq)
+  apply blast
+  done
 
 lemma (in uniform_space) controlled_sequences_convergent_imp_complete_aux_sequence:
   fixes U :: "nat \<Rightarrow> ('a \<times> 'a) set"