author | boehmes |
Wed, 17 Aug 2016 10:26:12 +0200 | |
changeset 63712 | 2606e8c8487d |
parent 63711 | e4843a8a8b18 (diff) |
parent 63710 | a2dffa971ec6 (current diff) |
child 63713 | 009e176e1010 |
--- a/src/HOL/Rat.thy Wed Aug 17 09:46:32 2016 +0200 +++ b/src/HOL/Rat.thy Wed Aug 17 10:26:12 2016 +0200 @@ -655,6 +655,7 @@ @{thm divide_1}, @{thm divide_zero_left}, @{thm times_divide_eq_right}, @{thm times_divide_eq_left}, @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym, + @{thm add_divide_distrib}, @{thm diff_divide_distrib}, @{thm of_int_minus}, @{thm of_int_diff}, @{thm of_int_of_nat_eq}] #> Lin_Arith.add_simprocs [Numeral_Simprocs.field_divide_cancel_numeral_factor]