src/HOL/Euclidean_Division.thy

--- a/src/HOL/Euclidean_Division.thy	Mon Apr 05 22:46:41 2021 +0200
+++ b/src/HOL/Euclidean_Division.thy	Tue Apr 06 18:12:20 2021 +0000
@@ -1625,8 +1625,8 @@
   obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
     by (blast intro: int_sgnE elim: that)
   with that show ?thesis
-    by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg
-      sgn_mult mod_eq_0_iff_dvd)
+    by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg sgn_mult)
+      (simp add: dvd_eq_mod_eq_0)
 qed
 
 instance proof