# HG changeset patch
# User wenzelm
# Date 1706731852 -3600
# Node ID 5c2c8a60b77e435a2fad3d474aaf18a4f3d6c9b6
# Parent  cd9ede8488afc830ade49d4c4b06321d095223f9
tuned proof: avoid z3;

diff -r cd9ede8488af -r 5c2c8a60b77e src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Wed Jan 31 19:17:45 2024 +0100
+++ b/src/HOL/Library/Float.thy	Wed Jan 31 21:10:52 2024 +0100
@@ -2310,7 +2310,8 @@
   "floor_fl (Float m e) = (if 0 \<le> e then Float m e else Float (m div (2 ^ (nat (-e)))) 0)"
   apply transfer
   apply (simp add: powr_int floor_divide_of_int_eq)
-  by (smt (z3) floor_divide_of_int_eq of_int_1 of_int_add of_int_power)
+  apply (metis floor_divide_of_int_eq of_int_eq_numeral_power_cancel_iff)
+  done
 
 end