src/HOL/Divides.thy

--- a/src/HOL/Divides.thy	Sat Oct 15 23:07:47 2016 +0200
+++ b/src/HOL/Divides.thy	Sun Oct 16 09:31:03 2016 +0200
@@ -2219,8 +2219,6 @@
   shows "divmod_int_rel (1 + 2*a) (2*b) (q, 1 + 2*r)"
   using assms unfolding divmod_int_rel_def by auto
 
-declaration \<open>K (Lin_Arith.add_simps @{thms uminus_numeral_One})\<close>
-
 lemma neg_divmod_int_rel_mult_2:
   assumes "b \<le> 0"
   assumes "divmod_int_rel (a + 1) b (q, r)"