--- 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