# HG changeset patch
# User haftmann
# Date 1534941178 0
# Node ID c7ee984243fcdb4e1410d3fa25852dd17b942437
# Parent  248e1678ce556c3b7878d6d2bd5cb1aed454655f
tuned

diff -r 248e1678ce55 -r c7ee984243fc src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Wed Aug 22 12:32:58 2018 +0000
+++ b/src/HOL/Binomial.thy	Wed Aug 22 12:32:58 2018 +0000
@@ -572,7 +572,7 @@
   have "(\<Sum>k\<le>r. (m choose k) * (0 choose (r - k))) = (\<Sum>k\<le>r. if k = r then (m choose k) else 0)"
     by (intro sum.cong) simp_all
   also have "\<dots> = m choose r"
-    by (simp add: sum.delta)
+    by simp
   finally show ?case
     by simp
 next
@@ -636,7 +636,7 @@
   have x: "0 \<le> x"
     using assms of_nat_0_le_iff order_trans by blast
   have "(x / of_nat k :: 'a) ^ k = (\<Prod>i = 0..<k. x / of_nat k :: 'a)"
-    by (simp add: prod_constant)
+    by simp
   also have "\<dots> \<le> x gchoose k" (* FIXME *)
     unfolding gbinomial_altdef_of_nat
     apply (safe intro!: prod_mono)