# HG changeset patch
# User wenzelm
# Date 1717708799 -7200
# Node ID 360e6217cda61d8c76455195ccc281fb84b9c9cb
# Parent  c631a44e9f132d01b1ecf44b36cc8e7e9d1be41f
tuned proof: avoid smt/z3 to make this work with arm64-linux;

diff -r c631a44e9f13 -r 360e6217cda6 src/HOL/Binomial_Plus.thy
--- a/src/HOL/Binomial_Plus.thy	Thu Jun 06 23:12:04 2024 +0200
+++ b/src/HOL/Binomial_Plus.thy	Thu Jun 06 23:19:59 2024 +0200
@@ -223,7 +223,7 @@
 proof -
   have dvd: "y \<noteq> 0 \<Longrightarrow> ((of_int (x div y))::'a::field_char_0) = of_int x / of_int y \<Longrightarrow> y dvd x"
     for x y :: int
-    by (smt dvd_triv_left mult.commute nonzero_eq_divide_eq of_int_eq_0_iff of_int_eq_iff of_int_mult)
+    by (metis dvd_triv_right nonzero_eq_divide_eq of_int_0_eq_iff of_int_eq_iff of_int_mult)
   show ?thesis
   proof (cases "0 < a")
     case True