# HG changeset patch
# User haftmann
# Date 1476603063 -7200
# Node ID b60a9752b6d097412291f67739ed1822c43b8111
# Parent  c1b5165b73dbebbc84d7dfa07f7feec932e43aaf
de-orphanized declaration

diff -r c1b5165b73db -r b60a9752b6d0 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)"
diff -r c1b5165b73db -r b60a9752b6d0 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Sat Oct 15 23:07:47 2016 +0200
+++ b/src/HOL/Num.thy	Sun Oct 16 09:31:03 2016 +0200
@@ -1217,7 +1217,7 @@
   K (
     Lin_Arith.add_simps
       @{thms arith_simps more_arith_simps rel_simps pred_numeral_simps
-        arith_special numeral_One of_nat_simps}
+        arith_special numeral_One of_nat_simps uminus_numeral_One}
     #> Lin_Arith.add_simps
       @{thms Suc_numeral Let_numeral Let_neg_numeral Let_0 Let_1
         le_Suc_numeral le_numeral_Suc less_Suc_numeral less_numeral_Suc