# HG changeset patch
# User boehmes
# Date 1471422372 -7200
# Node ID 2606e8c8487d2293e1c2d61de7058de40090341c
# Parent  e4843a8a8b18545a3ad9383a81fe5c3faec9d067# Parent  a2dffa971ec65e96384f972ca2fdebfdf12fb3cc
merged

diff -r a2dffa971ec6 -r 2606e8c8487d src/HOL/Rat.thy
--- 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]