diff -r 19f627407264 -r ccab07d1196c src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Euclidean_Division.thy	Sat Dec 02 16:50:53 2017 +0000
@@ -1432,7 +1432,7 @@
       then int (m div n)
       else - int (m div n + of_bool (\<not> n dvd m)))"
   by (auto simp add: divide_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
-    nat_mult_distrib dvd_int_iff)
+    nat_mult_distrib)
 
 instance proof
   fix k :: int show "k div 0 = 0"
@@ -1460,7 +1460,7 @@
     fix q
     assume "q dvd m" "q dvd n"
     then have "int q dvd int m" "int q dvd int n"
-      by (simp_all add: zdvd_int)
+      by simp_all
     with \<open>?P\<close> have "is_unit (int q)"
       by (rule coprime_common_divisor)
     then show "is_unit q"
@@ -1473,7 +1473,7 @@
     fix k
     assume "k dvd int m" "k dvd int n"
     then have "nat \<bar>k\<bar> dvd m" "nat \<bar>k\<bar> dvd n"
-      by (simp_all add: zdvd_int)
+      by simp_all
     with \<open>?Q\<close> have "is_unit (nat \<bar>k\<bar>)"
       by (rule coprime_common_divisor)
     then show "is_unit k"
@@ -1525,7 +1525,7 @@
       then sgn l * int (m mod n)
       else sgn l * (int (n * of_bool (\<not> n dvd m)) - int (m mod n)))"
   by (auto simp add: modulo_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
-    nat_mult_distrib dvd_int_iff)
+    nat_mult_distrib)
 
 instance proof
   fix k l :: int
@@ -1574,7 +1574,7 @@
     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 int_dvd_iff)
+      sgn_mult mod_eq_0_iff_dvd)
 qed
 
 instance proof