src/HOL/Divides.thy

--- a/src/HOL/Divides.thy	Sun Mar 11 21:08:47 2018 +0100
+++ b/src/HOL/Divides.thy	Mon Mar 12 08:25:35 2018 +0000
@@ -901,9 +901,6 @@
     by simp
 qed
 
-instance int :: semiring_bits
-  by standard (simp_all add: pos_zmod_mult_2 pos_zdiv_mult_2 zdiv_zmult2_eq zmod_zmult2_eq)
-
   
 subsubsection \<open>Quotients of Signs\<close>