--- 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)"
--- 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