diff -r 7611c55c39d0 -r 917ae0ba03a2 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Wed Mar 15 21:52:04 2017 +0100
+++ b/src/HOL/Set_Interval.thy	Thu Mar 16 13:55:29 2017 +0000
@@ -709,7 +709,7 @@
 
 subsubsection \<open>The Constant @{term greaterThan}\<close>
 
-lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"
+lemma greaterThan_0: "greaterThan 0 = range Suc"
 apply (simp add: greaterThan_def)
 apply (blast dest: gr0_conv_Suc [THEN iffD1])
 done
@@ -1846,6 +1846,12 @@
   shows "(\<Sum>i = m..n. f(Suc i) - f i) = f (Suc n) - f m"
 using assms by (induct n) (auto simp: le_Suc_eq)
 
+lemma sum_Suc_diff':
+  fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
+  assumes "m \<le> n"
+  shows "(\<Sum>i = m..<n. f (Suc i) - f i) = f n - f m"
+using assms by (induct n) (auto simp: le_Suc_eq)
+
 lemma nested_sum_swap:
      "(\<Sum>i = 0..n. (\<Sum>j = 0..<i. a i j)) = (\<Sum>j = 0..<n. \<Sum>i = Suc j..n. a i j)"
   by (induction n) (auto simp: sum.distrib)