diff -r 6e85281177df -r 26a1d66b9077 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Mon May 10 14:28:37 2021 +0200
+++ b/src/HOL/Library/Float.thy	Mon May 10 16:14:34 2021 +0200
@@ -2122,7 +2122,7 @@
     proof cases
       assume [simp]: "even j"
       have "a * power_down prec a j \<le> b * power_down prec b j"
-        by (smt IH(1) IH(2) \<open>even j\<close> lessI mult_mono' mult_mono_nonpos_nonneg power_down_even_nonneg)
+        by (metis IH(1) IH(2) \<open>even j\<close> lessI linear mult_mono mult_mono' mult_mono_nonpos_nonneg power_down_even_nonneg)
       then have "truncate_down (Suc prec) (a * power_down prec a j) \<le> truncate_down (Suc prec) (b * power_down prec b j)"
         by (auto intro!: truncate_down_mono simp: abs_le_square_iff[symmetric] abs_real_def)
       then show ?thesis
@@ -2193,7 +2193,7 @@
     proof cases
       assume [simp]: "even j"
       have "a * power_up prec a j \<le> b * power_up prec b j"
-        by (smt IH(1) IH(2) \<open>even j\<close> lessI mult_mono' mult_mono_nonpos_nonneg power_up_even_nonneg)
+        by (metis IH(1) IH(2) \<open>even j\<close> lessI linear mult_mono mult_mono' mult_mono_nonpos_nonneg power_up_even_nonneg)
       then have "truncate_up prec (a * power_up prec a j) \<le> truncate_up prec (b * power_up prec b j)"
         by (auto intro!: truncate_up_mono simp: abs_le_square_iff[symmetric] abs_real_def)
       then show ?thesis