# HG changeset patch
# User wenzelm
# Date 1706725065 -3600
# Node ID cd9ede8488afc830ade49d4c4b06321d095223f9
# Parent  58e974ef06255ee64a0b87d3fca46922a0ab0852
tuned proof: avoid z3 to make it work on arm64-linux;

diff -r 58e974ef0625 -r cd9ede8488af src/HOL/ex/BigO.thy
--- a/src/HOL/ex/BigO.thy	Wed Jan 31 16:55:16 2024 +0100
+++ b/src/HOL/ex/BigO.thy	Wed Jan 31 19:17:45 2024 +0100
@@ -271,7 +271,7 @@
   by (metis equalityI bigo_const2 bigo_const4)
 
 lemma bigo_const_mult1: "(\<lambda>x. c * f x) \<in> O(f)"
-  by (smt (z3) abs_mult bigo_def bigo_refl mem_Collect_eq mult.left_commute mult_commute_abs)
+  by (simp add: bigo_def) (metis abs_mult dual_order.refl)
 
 lemma bigo_const_mult2: "O(\<lambda>x. c * f x) \<subseteq> O(f)"
   by (metis bigo_elt_subset bigo_const_mult1)