# HG changeset patch
# User nipkow
# Date 1504800101 -7200
# Node ID 84926115c2ddf348052aeb86470180890743c133
# Parent  a61181ffb1ce70a092e7c6bb46709eb35cf45ec8# Parent  c375b64a6c24926ff9379223c94413abd7763f60
merged

diff -r a61181ffb1ce -r 84926115c2dd src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Thu Sep 07 13:13:10 2017 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu Sep 07 18:01:41 2017 +0200
@@ -752,7 +752,7 @@
 lemma e_approx_32: "\<bar>exp(1) - 5837465777 / 2147483648\<bar> \<le> (inverse(2 ^ 32)::real)"
   using Taylor_exp [of 1 14] exp_le
   apply (simp add: sum_distrib_right in_Reals_norm Re_exp atMost_nat_numeral fact_numeral)
-  apply (simp only: pos_le_divide_eq [symmetric], linarith)
+  apply (simp only: pos_le_divide_eq [symmetric])
   done
 
 lemma e_less_272: "exp 1 < (272/100::real)"
diff -r a61181ffb1ce -r 84926115c2dd src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Thu Sep 07 13:13:10 2017 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Thu Sep 07 18:01:41 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}])