# HG changeset patch
# User nipkow
# Date 1504789960 -7200
# Node ID 98b7ba7b1e9a026ce0884b3b6077da8360be2904
# Parent  a8edca8c4a680ded543a45a69f50cba7d8bbbbf7
more simp power and less incompleteness or arith

diff -r a8edca8c4a68 -r 98b7ba7b1e9a src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Tue Sep 05 20:03:52 2017 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Thu Sep 07 15:12:40 2017 +0200
@@ -975,6 +975,7 @@
   #> add_discrete_type @{type_name nat}
   #> add_lessD @{thm Suc_leI}
   #> add_simps (@{thms simp_thms} @ @{thms ring_distribs} @ [@{thm if_True}, @{thm if_False},
+      @{thm minus_diff_eq},
       @{thm add_0_left}, @{thm add_0_right}, @{thm order_less_irrefl},
       @{thm zero_neq_one}, @{thm zero_less_one}, @{thm zero_le_one},
       @{thm zero_neq_one} RS not_sym, @{thm not_one_le_zero}, @{thm not_one_less_zero}])