diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Wed Oct 09 23:00:52 2019 +0200
+++ b/src/HOL/Library/Float.thy	Wed Oct 09 14:51:54 2019 +0000
@@ -492,13 +492,13 @@
 qed
 
 lemma mantissa_pos_iff: "0 < mantissa x \<longleftrightarrow> 0 < x"
-  by (auto simp: mantissa_exponent sign_simps)
+  by (auto simp: mantissa_exponent algebra_split_simps)
 
 lemma mantissa_nonneg_iff: "0 \<le> mantissa x \<longleftrightarrow> 0 \<le> x"
-  by (auto simp: mantissa_exponent sign_simps)
+  by (auto simp: mantissa_exponent algebra_split_simps)
 
 lemma mantissa_neg_iff: "0 > mantissa x \<longleftrightarrow> 0 > x"
-  by (auto simp: mantissa_exponent sign_simps)
+  by (auto simp: mantissa_exponent algebra_split_simps)
 
 lemma
   fixes m e :: int
@@ -1139,7 +1139,7 @@
       auto
         intro!: floor_eq2
         intro: powr_strict powr
-        simp: powr_diff powr_add divide_simps algebra_simps)+
+        simp: powr_diff powr_add field_split_simps algebra_simps)+
   finally
   show ?thesis by simp
 qed