de-orphanized declaration
authorhaftmann
Sun Oct 16 09:31:03 2016 +0200 (2016-10-16)
changeset 64238b60a9752b6d0
parent 64237 c1b5165b73db
child 64239 de5cd9217d4c
de-orphanized declaration
src/HOL/Divides.thy
src/HOL/Num.thy
     1.1 --- a/src/HOL/Divides.thy	Sat Oct 15 23:07:47 2016 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sun Oct 16 09:31:03 2016 +0200
     1.3 @@ -2219,8 +2219,6 @@
     1.4    shows "divmod_int_rel (1 + 2*a) (2*b) (q, 1 + 2*r)"
     1.5    using assms unfolding divmod_int_rel_def by auto
     1.6  
     1.7 -declaration \<open>K (Lin_Arith.add_simps @{thms uminus_numeral_One})\<close>
     1.8 -
     1.9  lemma neg_divmod_int_rel_mult_2:
    1.10    assumes "b \<le> 0"
    1.11    assumes "divmod_int_rel (a + 1) b (q, r)"
     2.1 --- a/src/HOL/Num.thy	Sat Oct 15 23:07:47 2016 +0200
     2.2 +++ b/src/HOL/Num.thy	Sun Oct 16 09:31:03 2016 +0200
     2.3 @@ -1217,7 +1217,7 @@
     2.4    K (
     2.5      Lin_Arith.add_simps
     2.6        @{thms arith_simps more_arith_simps rel_simps pred_numeral_simps
     2.7 -        arith_special numeral_One of_nat_simps}
     2.8 +        arith_special numeral_One of_nat_simps uminus_numeral_One}
     2.9      #> Lin_Arith.add_simps
    2.10        @{thms Suc_numeral Let_numeral Let_neg_numeral Let_0 Let_1
    2.11          le_Suc_numeral le_numeral_Suc less_Suc_numeral less_numeral_Suc